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

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

then A3: 0 + 1 <= len f by NAT_1:13;
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: len <%(f . 0 )%> = 0 + 1 by AFINSQ_1:38;
A34: f . 0 = <%(f . 0 )%> . 0 by AFINSQ_1:38;
set d = f . 0 ;
set g2 = <%(f . 0 )%>;
for i being Nat st i + 1 < 0 + 1 holds
<%(f . 0 )%> . (i + 1) = (<%(f . 0 )%> . i) + (f . (i + 1)) by XREAL_1:8;
then A31: S₁[ 0 ] by A2, A34;
A32: 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
B2: ( len g3 = k + 1 & f . 0 = g3 . 0 & ( 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 C1: 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)))%>;
C2: 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 ;
C4: 0 in dom g3 by B2, NAT_1:45;
C5: (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . 0 = g3 . 0 by C4, AFINSQ_1:def 4;
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 D2: i + 1 <= k + 1 by NAT_1:13;

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

suppose E1: 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 + 1 in dom g3 by E1, B2, NAT_1:45;
then E3: (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . (i + 1) = g3 . (i + 1) by AFINSQ_1:def 4;
i <= i + 1 by NAT_1:11;
then i < len g3 by B2, E1, XXREAL_0:2;
then i in dom g3 by NAT_1:45;
then (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . i = g3 . i 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 E3, B2, E1, C1; :: thesis: verum

end;

suppose E0: 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 E0, B2, NAT_1:45;
then E4: (g3 ^ <%((g3 . ((len g3) -' 1)) + (f . (len g3)))%>) . i = g3 . i by AFINSQ_1:def 4;
(len g3) -' 1 = i by E0, B2, 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 B2, E0, E4, AFINSQ_1:40; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] by C2, C5, B2; :: thesis: verum

end;

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

reconsider O = 0 as Element of REAL ;
set r = <%O%>;
set g4 = g3 ^ <%O%>;
C2: len (g3 ^ <%O%>) = (len g3) + (len <%0 %>) by AFINSQ_1:20
.= (len g3) + 1 by AFINSQ_1:38 ;
then C3: len (g3 ^ <%O%>) > len f by C1, NAT_1:13;
C4: 0 in dom g3 by B1, C1, NAT_1:45;
(g3 ^ <%O%>) . 0 = g3 . 0 by C4, AFINSQ_1:def 4;
hence S₁[k + 1] by B2, C3, C2; :: thesis: verum

end;

end;

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A31, A32);
then consider g being XFinSequence of such that
A33: ( len g = ((len f) -' 1) + 1 & f . 0 = g . 0 & ( 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)) ) ) ;
A34: ((len f) -' 1) + 1 = ((len f) - 1) + 1 by A3, XREAL_1:235
.= len f ;
set b = g . ((len f) -' 1);
( 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)) ) & g . ((len f) -' 1) = g . ((len f) -' 1) ) by A34, A33;
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) ) ; :: thesis: verum

end;

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