let e be FinSequence of REAL ; :: thesis: ( len e >= 1 & ( 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 being Nat st n in dom e holds
e . n <= f . n )
assume that
A1: len e >= 1 and
A2: 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 being Nat st n in dom e holds
e . n <= f . n
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 being Nat st n in dom e holds
e . n <= f . n )
assume A3: ( 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 being Nat st n in dom e holds
e . n <= f . n
defpred S₁[ Nat] means ( $1 in dom e implies e . $1 <= f . $1 );
A4: S₁[ 0 ] by FINSEQ_3:27;

A5: now

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

now

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

per cases ( ( k = 0 & k < len e ) or ( k > 0 & k < len e ) ) by A6, NAT_1:13;

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

hence e . (k + 1) <= f . (k + 1) by A3; :: thesis: verum

end;

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

then ( 1 <= len e & k >= 1 & k <= len e ) by NAT_1:14;
then ( 1 in dom e & k in dom e & k >= 1 ) by FINSEQ_3:27;
then A8: e . 1 <= f . k by A2, A3, Th3;
1 in dom e by A1, FINSEQ_3:27;
then f . k >= 0 by A2, A8;
then (f . k) + (e . (k + 1)) >= e . (k + 1) by XREAL_1:33;
hence e . (k + 1) <= f . (k + 1) by A3, A7; :: thesis: verum

end;

end;

end;

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

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A5);
hence for n being Nat st n in dom e holds
e . n <= f . n ; :: thesis: verum