for e being real-valued FinSequence st ( for i being Nat st i in dom e holds
0 <= e . i ) holds
for f being Real_Sequence st ( for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) holds
for n, m being Nat st n in dom e & m in dom e & n <= m holds
f . n <= f . m