let e be real-valued FinSequence; ( 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
; 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; ( 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 that
A3:
f . 1 = e . 1
and
A4:
for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1))
; for n being Nat st n in dom e holds
e . n <= f . n
defpred S1[ Nat] means ( $1 in dom e implies e . $1 <= f . $1 );
A5:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume
S1[
k]
;
S1[k + 1]now ( k + 1 in dom e implies e . (k + 1) <= f . (k + 1) )assume
k + 1
in dom e
;
e . (k + 1) <= f . (k + 1)then A6:
k + 1
<= len e
by FINSEQ_3:25;
per cases
( ( k = 0 & k < len e ) or ( k > 0 & k < len e ) )
by A6, NAT_1:13;
suppose A7:
(
k > 0 &
k < len e )
;
e . (k + 1) <= f . (k + 1)then
1
<= len e
by NAT_1:14;
then A8:
1
in dom e
by FINSEQ_3:25;
A9:
1
in dom e
by A1, FINSEQ_3:25;
A10:
k >= 1
by A7, NAT_1:14;
then
k in dom e
by A7, FINSEQ_3:25;
then
e . 1
<= f . k
by A2, A3, A4, A10, A8, Th3;
then
f . k >= 0
by A2, A9;
then
(f . k) + (e . (k + 1)) >= e . (k + 1)
by XREAL_1:31;
hence
e . (k + 1) <= f . (k + 1)
by A4, A7;
verum end; end; end; hence
S1[
k + 1]
;
verum end;
A11:
S1[ 0 ]
by FINSEQ_3:25;
for n being Nat holds S1[n]
from NAT_1:sch 2(A11, A5);
hence
for n being Nat st n in dom e holds
e . n <= f . n
; verum