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

proof

let n be Nat; :: thesis: ( n <> 0 & n < len e implies f . n <= f . (n + 1) )
assume that
A4: n <> 0 and
A5: n < len e ; :: thesis: f . n <= f . (n + 1)
( 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: verum

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: ( n in dom e implies for m being Nat st m in dom e & n <= m holds
f . n <= f . m )
assume n in dom e ; :: thesis: for m being Nat st m in dom e & n <= m holds
f . n <= f . m
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: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: ( k + 1 in dom e & n <= k + 1 implies f . (k + 1) >= f . n )

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

per cases ( ( k + 1 = n & k < len e ) or ( k >= n & k < len e ) ) by A10, A11, NAT_1:8, NAT_1:13;

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

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

end;

suppose A12: ( k >= n & k < len e ) ; :: thesis: f . (k + 1) >= f . n

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: verum

end;

end;

end;

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

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: verum

end;

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