let e be real-valued FinSequence; :: thesis:
assume A1: for i being Nat st i in dom e holds
0 <= e . i ; :: thesis:
let f be Real_Sequence; :: thesis:
assume A2: for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ; :: thesis:
A3: for n being Nat st n <> 0 & n < len e holds
f . n <= f . (n + 1)

proof

let n be Nat; :: thesis:
assume that
A4: n <> 0 and
A5: n < len e ; :: thesis:
( n + 1 >= 1 & n + 1 <= len e ) by A5, NAT_1:13, NAT_1:14;
then n + 1 in dom e by FINSEQ_3:25;
then (f . n) + (e . (n + 1)) >= f . n by A1, XREAL_1:31;
hence f . n <= f . (n + 1) by A2, A4, A5; :: thesis:

end;

for n being Nat st n in dom e holds
for m being Nat st m in dom e & n <= m holds
f . n <= f . m

proof

let n be Nat; :: thesis:
assume n in dom e ; :: thesis:
then A6: n >= 1 by FINSEQ_3:25;
defpred S₁[ Nat] means ( $1 in dom e & n <= $1 implies f . $1 >= f . n );

A7: now :: thesis:

let k be Nat; :: thesis:
assume A8: S₁[k] ; :: thesis:

now :: thesis:

assume that
A9: k + 1 in dom e and
A10: n <= k + 1 ; :: thesis:
A11: k + 1 <= len e by A9, FINSEQ_3:25;

per cases by A10, A11, NAT_1:8, NAT_1:13;

suppose ( k + 1 = n & k < len e ) ; :: thesis:

hence f . (k + 1) >= f . n ; :: thesis:

end;

suppose A12: ( k >= n & k < len e ) ; :: thesis:

then ( k >= 1 & f . (k + 1) >= f . k ) by A3, A6, NAT_1:14;
hence f . (k + 1) >= f . n by A8, A12, FINSEQ_3:25, XXREAL_0:2; :: thesis:

end;

end;

end;

hence S₁[k + 1] ; :: thesis:

end;

A13: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A7);
hence for m being Nat st m in dom e & n <= m holds
f . n <= f . m ; :: thesis:

end;

hence for n, m being Nat st n in dom e & m in dom e & n <= m holds
f . n <= f . m ; :: thesis: