let e be FinSequence of REAL ; :: thesis: ( ( for i being Nat st i in dom e holds
0 <= e . i ) implies 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, 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 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, 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: ( f . 1 = e . 1 & ( 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: ( f . 1 = e . 1 & ( 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 A4: ( n <> 0 & n < len e ) ; :: thesis: f . n <= f . (n + 1)
( n + 1 >= 1 & n + 1 <= len e ) by A4, NAT_1:13, NAT_1:14;
then n + 1 in dom e by FINSEQ_3:27;
then (f . n) + (e . (n + 1)) >= f . n by A1, XREAL_1:33;
hence f . n <= f . (n + 1) by A2, A4; :: 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 A5: n in dom e ; :: thesis: for m being Nat st m in dom e & n <= m holds
f . n <= f . m
A6: ( n >= 1 & n <= len e ) by A5, FINSEQ_3:27;
defpred S₁[ Nat] means ( $1 in dom e & n <= $1 implies f . $1 >= f . n );
A7: S₁[ 0 ] ;

A8: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]

now

assume ( k + 1 in dom e & n <= k + 1 ) ; :: thesis: f . (k + 1) >= f . n
then A10: ( k + 1 >= n & k + 1 <= len e ) by FINSEQ_3:27;

per cases ( ( k + 1 = n & k < len e ) or ( k >= n & k < len e ) ) by A10, 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 A11: ( k >= n & k < len e ) ; :: thesis: f . (k + 1) >= f . n

then ( k >= 1 & k < len e ) by A6, NAT_1:14;
then ( f . (k + 1) >= f . k & f . k >= f . n ) by A3, A9, A11, FINSEQ_3:27;
hence f . (k + 1) >= f . n by XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A7, A8);
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