for fs being FinSequence of REAL
for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) holds
Sum (Seq fss) <= Sum fs