theorem Th4: :: MATRPROB:4

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