per cases ( len f > 0 or not len f > 0 ) ;

suppose A1: len f > 0 ; :: thesis: ex b₁ being Element of REAL ex g being XFinSequence of st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & b₁ = g . ((len f) -' 1) )

defpred S₁[ Nat] means ex g being XFinSequence of st
( len g = $1 + 1 & f . 0 = g . 0 & ( len g <= len f implies for i being Nat st i + 1 < $1 + 1 holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) );
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider g3 being XFinSequence of such that
A3: len g3 = k + 1 and
A4: f . 0 = g3 . 0 and
A5: ( len g3 <= len f implies for i being Nat st i + 1 < k + 1 holds
g3 . (i + 1) = (g3 . i) + (f . (i + 1)) ) ;

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

suppose A6: len g3 < len f ; :: thesis: S₁[k + 1]

set O = (g3 . ((len g3) -' 1)) + (f . (len g3));
set r = <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>;
set g4 = g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>;
A7: for i being Nat st i + 1 < (k + 1) + 1 holds
(g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . (i + 1) = ((g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . i) + (f . (i + 1))

proof

let i be Nat; :: thesis: ( i + 1 < (k + 1) + 1 implies (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . (i + 1) = ((g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . i) + (f . (i + 1)) )
assume i + 1 < (k + 1) + 1 ; :: thesis: (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . (i + 1) = ((g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . i) + (f . (i + 1))
then A8: i + 1 <= k + 1 by NAT_1:13;

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

suppose A9: i + 1 < k + 1 ; :: thesis: (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . (i + 1) = ((g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . i) + (f . (i + 1))

i <= i + 1 by NAT_1:11;
then i < len g3 by A3, A9, XXREAL_0:2;
then i in dom g3 by NAT_1:45;
then A10: (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . i = g3 . i by AFINSQ_1:def 4;
i + 1 in dom g3 by A3, A9, NAT_1:45;
then (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . (i + 1) = g3 . (i + 1) by AFINSQ_1:def 4;
hence (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . (i + 1) = ((g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . i) + (f . (i + 1)) by A5, A6, A9, A10; :: thesis: verum

end;

suppose A11: i + 1 = k + 1 ; :: thesis: (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . (i + 1) = ((g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . i) + (f . (i + 1))

i < i + 1 by XREAL_1:31;
then i in dom g3 by A3, A11, NAT_1:45;
then A12: (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . i = g3 . i by AFINSQ_1:def 4;
(len g3) -' 1 = i by A3, A11, NAT_D:34;
hence (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . (i + 1) = ((g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . i) + (f . (i + 1)) by A3, A11, A12, AFINSQ_1:40; :: thesis: verum

end;

end;

end;

0 in dom g3 by A3, NAT_1:45;
then A13: (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . 0 = g3 . 0 by AFINSQ_1:def 4;
len (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) = (len g3) + (len <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) by AFINSQ_1:20
.= (len g3) + 1 by AFINSQ_1:38 ;
hence S₁[k + 1] by A3, A4, A13, A7; :: thesis: verum

end;

suppose A14: len g3 >= len f ; :: thesis: S₁[k + 1]

reconsider O = 0 as Element of REAL ;
set r = <%O%>;
set g4 = g3 ^ <%O%>;
0 in dom g3 by A1, A14, NAT_1:45;
then A15: (g3 ^ <%O%>) . 0 = g3 . 0 by AFINSQ_1:def 4;
A16: len (g3 ^ <%O%>) = (len g3) + (len <%0 %>) by AFINSQ_1:20
.= (len g3) + 1 by AFINSQ_1:38 ;
then len (g3 ^ <%O%>) > len f by A14, NAT_1:13;
hence S₁[k + 1] by A3, A4, A16, A15; :: thesis: verum

end;

end;

end;

set d = f . 0 ;
A17: f . 0 = <%(f . 0 )%> . 0 by AFINSQ_1:38;
set g2 = <%(f . 0 )%>;
A18: for i being Nat st i + 1 < 0 + 1 holds
<%(f . 0 )%> . (i + 1) = (<%(f . 0 )%> . i) + (f . (i + 1)) by XREAL_1:8;
0 + 1 <= len f by A1, NAT_1:13;
then A19: ((len f) -' 1) + 1 = ((len f) - 1) + 1 by XREAL_1:235
.= len f ;
len <%(f . 0 )%> = 0 + 1 by AFINSQ_1:38;
then A20: S₁[ 0 ] by A17, A18;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A20, A2);
then consider g being XFinSequence of such that
A21: len g = ((len f) -' 1) + 1 and
A22: f . 0 = g . 0 and
A23: ( len g <= len f implies for i being Nat st i + 1 < ((len f) -' 1) + 1 holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) ;
set b = g . ((len f) -' 1);
g . ((len f) -' 1) = g . ((len f) -' 1) ;
hence ex b₁ being Element of REAL ex g being XFinSequence of st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & b₁ = g . ((len f) -' 1) ) by A21, A22, A23, A19; :: thesis: verum

end;

suppose A24: not len f > 0 ; :: thesis: ex b₁ being Element of REAL ex g being XFinSequence of st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & b₁ = g . ((len f) -' 1) )

take 0 ; :: thesis: ex g being XFinSequence of st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & 0 = g . ((len f) -' 1) )
take g = <%> REAL ; :: thesis: ( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & 0 = g . ((len f) -' 1) )
len f = 0 by A24;
hence ( len f = len g & f . 0 = g . 0 ) by AFINSQ_1:18; :: thesis: ( ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & 0 = g . ((len f) -' 1) )
thus for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) by A24; :: thesis: 0 = g . ((len f) -' 1)
not 0 in dom g ;
hence 0 = g . ((len f) -' 1) by FUNCT_1:def 4; :: thesis: verum

end;

end;