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

suppose A1: 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 ) )

reconsider q = <*(f /. 1)*> as FinSequence of REAL n ;
A2: 0 + 1 <= len f by A1, NAT_1:13;
then f /. 1 = f . 1 by FINSEQ_4:24;
then A3: q . 1 = f . 1 by FINSEQ_1:57;
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)) ) ) );
A4: for i being Nat st 1 <= i & i < 0 + 1 holds
q . (i + 1) = (q /. i) + (f /. (i + 1)) ;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

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

suppose A7: (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
A8: k + 1 = len g and
A9: f . 1 = g . 1 and
A10: for i being Nat st 1 <= i & i < k + 1 holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) by A6, A7, XXREAL_0:2;
reconsider g2 = g ^ <*((g /. (k + 1)) + (f /. ((k + 1) + 1)))*> as FinSequence of REAL n ;
A11: Seg (len g) = dom g by FINSEQ_1:def 3;
A12: len g2 = (len g) + (len <*((g /. (k + 1)) + (f /. ((k + 1) + 1)))*>) by FINSEQ_1:35
.= (k + 1) + 1 by A8, FINSEQ_1:57 ;
A13: 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 that
A14: 1 <= i and
A15: i < (k + 1) + 1 ; :: thesis: g2 . (i + 1) = (g2 /. i) + (f /. (i + 1))
A16: g2 /. i = g2 . i by A12, A14, A15, FINSEQ_4:24;
A17: i <= k + 1 by A15, NAT_1:13;
then A18: g /. i = g . i by A8, A14, FINSEQ_4:24;
i in Seg (len g) by A8, A14, A17, FINSEQ_1:3;
then A19: g . i = g2 . i by A11, FINSEQ_1:def 7;

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

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

A21: 1 <= i + 1 by NAT_1:12;
i + 1 <= k + 1 by A20, NAT_1:13;
then i + 1 in Seg (len g) by A8, A21, FINSEQ_1:3;
then g2 . (i + 1) = g . (i + 1) by A11, FINSEQ_1:def 7;
hence g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) by A10, A14, A19, A16, A18, A20; :: 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 A8, A19, A16, A18, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

1 <= k + 1 by NAT_1:11;
then 1 in Seg (len g) by A8, FINSEQ_1:3;
then g2 . 1 = f . 1 by A9, A11, FINSEQ_1:def 7;
hence S₁[k + 1] by A12, A13; :: thesis: verum

end;

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

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

end;

end;

end;

(len f) -' 1 = (len f) - 1 by A2, XREAL_1:235;
then A22: ((len f) -' 1) + 1 = len f ;
len q = 1 by FINSEQ_1:57;
then A23: S₁[ 0 ] by A3, A4;
for k being Nat holds S₁[k] from NAT_1:sch 2(A23, A5);
then consider g0 being FinSequence of REAL n such that
A24: len f = len g0 and
A25: f . 1 = g0 . 1 and
A26: for i being Nat st 1 <= i & i < len f holds
g0 . (i + 1) = (g0 /. i) + (f /. (i + 1)) by A22;
reconsider p0 = g0 /. (len f) as Element of REAL n ;
p0 = g0 . (len f) by A2, A24, 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 A24, A25, A26; :: 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;