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

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

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]

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

suppose 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;
then i in Seg (len g) by A9, A12, FINSEQ_1:3;
then A20: g . i = g2 . i by A0, FINSEQ_1:def 7;
A18: g2 /. i = g2 . i by A10, A12, FINSEQ_4:24;
A21: g /. i = g . i by A9, A12, A13, FINSEQ_4:24;

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 g2 . (i + 1) = g . (i + 1) by A0, FINSEQ_1:def 7;
hence g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) by A9, A12, A14, A18, A20, A21; :: thesis: verum

end;

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

hence g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) by A9, A18, A20, A21, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

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

end;

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

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

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
then consider g0 being FinSequence of REAL n such that
A22: ( len f = len g0 & f . 1 = g0 . 1 & ( for i being Nat st 1 <= i & i < len f holds
g0 . (i + 1) = (g0 /. i) + (f /. (i + 1)) ) ) by A3;
reconsider p0 = g0 /. (len f) as Element of REAL n ;
p0 = g0 . (len f) by A1, A22, FINSEQ_4:24;
hence ( ( len f > 0 implies ex p being Element of REAL n ex g being FinSequence of REAL n st
( len f = len g & f . 1 = g . 1 & ( for i being Nat st 1 <= i & i < len f holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) ) & p = g . (len f) ) ) & ( len f <= 0 implies ex p being Element of REAL n st p = 0* n ) ) by A22; :: thesis: verum

end;

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

hence ( ( len f > 0 implies ex p being Element of REAL n ex g being FinSequence of REAL n st
( len f = len g & f . 1 = g . 1 & ( for i being Nat st 1 <= i & i < len f holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) ) & p = g . (len f) ) ) & ( len f <= 0 implies ex p being Element of REAL n st p = 0* n ) ) ; :: thesis: verum

end;

end;