per cases ( len f > 0 or len f <= 0 ) ;

suppose len f > 0 ; :: thesis: ex b₁ being FinSequence of REAL n st
( len f = len b₁ & f . 1 = b₁ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₁ . (i + 1) = (b₁ /. i) + (f /. (i + 1)) ) )

then A1: 0 + 1 <= len f by NAT_1:13;
defpred S₁[ Nat] means ( $1 + 1 <= len f implies ex g being FinSequence of REAL n st
( $1 + 1 = len g & f . 1 = g . 1 & ( for i being Nat st 1 <= i & i < $1 + 1 holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) ) ) );
reconsider q = <*(f /. 1)*> as FinSequence of REAL n ;
A2: f /. 1 = f . 1 by A1, FINSEQ_4:24;
(len f) -' 1 = (len f) - 1 by A1, XREAL_1:235;
then A3: ((len f) -' 1) + 1 = len f ;
A4: ( len q = 1 & q . 1 = f . 1 ) by A2, FINSEQ_1:57;
for i being Nat st 1 <= i & i < 0 + 1 holds
q . (i + 1) = (q /. i) + (f /. (i + 1)) ;
then A5: S₁[ 0 ] by A4;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

now

per cases ( (k + 1) + 1 <= len f or (k + 1) + 1 > len f ) ;

case A8: (k + 1) + 1 <= len f ; :: thesis: S₁[k + 1]

k + 1 < (k + 1) + 1 by XREAL_1:31;
then consider g being FinSequence of REAL n such that
A9: ( k + 1 = len g & f . 1 = g . 1 & ( for i being Nat st 1 <= i & i < k + 1 holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) ) ) by A7, A8, XXREAL_0:2;
A0: Seg (len g) = dom g by FINSEQ_1:def 3;
reconsider g2 = g ^ <*((g /. (k + 1)) + (f /. ((k + 1) + 1)))*> as FinSequence of REAL n ;
A10: len g2 = (len g) + (len <*((g /. (k + 1)) + (f /. ((k + 1) + 1)))*>) by FINSEQ_1:35
.= (k + 1) + 1 by A9, FINSEQ_1:57 ;
1 <= k + 1 by NAT_1:11;
then 1 in Seg (len g) by A9, FINSEQ_1:3;
then A11: g2 . 1 = f . 1 by A0, A9, FINSEQ_1:def 7;
for i being Nat st 1 <= i & i < (k + 1) + 1 holds
g2 . (i + 1) = (g2 /. i) + (f /. (i + 1))

proof

let i be Nat; :: thesis: ( 1 <= i & i < (k + 1) + 1 implies g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) )
assume A12: ( 1 <= i & i < (k + 1) + 1 ) ; :: thesis: g2 . (i + 1) = (g2 /. i) + (f /. (i + 1))
then A13: i <= k + 1 by NAT_1:13;

per cases ( i < k + 1 or i = k + 1 ) by A13, XXREAL_0:1;

suppose A14: i < k + 1 ; :: thesis: g2 . (i + 1) = (g2 /. i) + (f /. (i + 1))

A15: 1 <= i + 1 by NAT_1:12;
i + 1 <= k + 1 by A14, NAT_1:13;
then i + 1 in Seg (len g) by A9, A15, FINSEQ_1:3;
then A16: g2 . (i + 1) = g . (i + 1) by A0, FINSEQ_1:def 7;
i in Seg (len g) by A9, A12, A13, FINSEQ_1:3;
then A17: g2 . i = g . i by A0, FINSEQ_1:def 7;
A18: g2 /. i = g2 . i by A10, A12, FINSEQ_4:24;
g /. i = g . i by A9, A12, A14, FINSEQ_4:24;
hence g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) by A9, A12, A14, A16, A17, A18; :: thesis: verum

end;

suppose A19: i = k + 1 ; :: thesis: g2 . (i + 1) = (g2 /. i) + (f /. (i + 1))

i in Seg (len g) by A9, A12, A13, FINSEQ_1:3;
then A20: g . i = g2 . i by A0, FINSEQ_1:def 7;
A21: g /. i = g . i by A9, A12, A13, FINSEQ_4:24;
g2 /. i = g2 . i by A10, A12, FINSEQ_4:24;
hence g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) by A9, A19, A20, A21, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] by A10, A11; :: thesis: verum

end;

case (k + 1) + 1 > len f ; :: thesis: S₁[k + 1]

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

end;

end;

end;

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

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
hence ex b₁ being FinSequence of REAL n st
( len f = len b₁ & f . 1 = b₁ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₁ . (i + 1) = (b₁ /. i) + (f /. (i + 1)) ) ) by A3; :: thesis: verum

end;

suppose A22: len f <= 0 ; :: thesis: ex b₁ being FinSequence of REAL n st
( len f = len b₁ & f . 1 = b₁ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₁ . (i + 1) = (b₁ /. i) + (f /. (i + 1)) ) )

take f ; :: thesis: ( len f = len f & f . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
f . (i + 1) = (f /. i) + (f /. (i + 1)) ) )
thus ( len f = len f & f . 1 = f . 1 ) ; :: thesis: for i being Nat st 1 <= i & i < len f holds
f . (i + 1) = (f /. i) + (f /. (i + 1))
let i be Nat; :: thesis: ( 1 <= i & i < len f implies f . (i + 1) = (f /. i) + (f /. (i + 1)) )
thus ( 1 <= i & i < len f implies f . (i + 1) = (f /. i) + (f /. (i + 1)) ) by A22; :: thesis: verum

end;

end;