defpred S₁[ set ] means for F being FinSequence of the carrier of V st len F = $1 holds
ex u being Element of V ex f being Function of NAT ,the carrier of V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) );

let n be Element of NAT ; :: thesis:
assume A1: for F being FinSequence of the carrier of V st len F = n holds
ex u being Element of V ex f being Function of NAT ,the carrier of V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) ; :: thesis:
let F be FinSequence of the carrier of V; :: thesis:
reconsider G = F | (Seg n) as FinSequence of the carrier of V by FINSEQ_1:23;
A2: rng F c= the carrier of V by FINSEQ_1:def 4;
assume A3: len F = n + 1 ; :: thesis:
then dom F = Seg (n + 1) by FINSEQ_1:def 3;
then n + 1 in dom F by FINSEQ_1:6;
then F . (n + 1) in rng F by FUNCT_1:def 5;
then reconsider u1 = F . (n + 1) as Element of V by A2;
A4: n < n + 1 by NAT_1:13;
then consider u being Element of V, f being Function of NAT ,the carrier of V such that
u = f . (len G) and
A5: f . 0 = 0. V and
A6: for j being Element of NAT
for v being Element of V st j < len G & v = G . (j + 1) holds
f . (j + 1) = (f . j) + v by A1, A3, FINSEQ_1:21;
defpred S₂[ set , set ] means for j being Element of NAT st $1 = j holds
( ( j < n + 1 implies $2 = f . $1 ) & ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
$2 = (f . (len G)) + u ) );
A7: for k being Element of NAT ex v being Element of V st S₂[k,v]

let k be Element of NAT ; :: thesis:
reconsider i = k as Element of NAT ;

A8: now

assume A9: n + 1 <= i ; :: thesis:
take v = (f . (len G)) + u1; :: thesis:
let j be Element of NAT ; :: thesis:
assume k = j ; :: thesis:
hence ( j < n + 1 implies v = f . k ) by A9; :: thesis:
assume n + 1 <= j ; :: thesis:
let u2 be Element of V; :: thesis:
assume u2 = F . (n + 1) ; :: thesis:
hence v = (f . (len G)) + u2 ; :: thesis:

end;

now

assume A10: i < n + 1 ; :: thesis:
take v = f . k; :: thesis:
let j be Element of NAT ; :: thesis:
assume A11: k = j ; :: thesis:
thus ( j < n + 1 implies v = f . k ) ; :: thesis:
thus ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
v = (f . (len G)) + u ) by A10, A11; :: thesis:

end;

hence ex v being Element of V st S₂[k,v] by A8; :: thesis:

end;

consider f' being Function of NAT ,the carrier of V such that
A12: for k being Element of NAT holds S₂[k,f' . k] from FUNCT_2:sch 3(A7);
take z = f' . (n + 1); :: thesis:
take f'' = f'; :: thesis:
thus z = f'' . (len F) by A3; :: thesis:
thus f'' . 0 = 0. V by A5, A12; :: thesis:
let j be Element of NAT ; :: thesis:
let v be Element of V; :: thesis:
assume that
A13: j < len F and
A14: v = F . (j + 1) ; :: thesis:
A15: len G = n by A3, A4, FINSEQ_1:21;

A16: now

assume A17: j = n ; :: thesis:
then f'' . (j + 1) = (f . j) + v by A15, A12, A14;
hence f'' . (j + 1) = (f'' . j) + v by A4, A12, A17; :: thesis:

end;

A18: now

assume A19: j < n ; :: thesis:
then A20: j + 1 < n + 1 by XREAL_1:8;
( 1 <= 1 + j & j + 1 <= n ) by A19, NAT_1:11, NAT_1:13;
then j + 1 in Seg n by FINSEQ_1:3;
then A21: v = G . (j + 1) by A14, FUNCT_1:72;
j < len G by A3, A4, A19, FINSEQ_1:21;
then A22: f . (j + 1) = (f . j) + v by A6, A21;
j < n + 1 by A19, NAT_1:13;
then f . (j + 1) = (f' . j) + v by A12, A22;
hence f'' . (j + 1) = (f'' . j) + v by A12, A20; :: thesis:

end;

j <= n by A3, A13, NAT_1:13;
hence f'' . (j + 1) = (f'' . j) + v by A18, A16, XXREAL_0:1; :: thesis:

end;

then A23: for n being Element of NAT st S₁[n] holds
S₁[n + 1] ;

reconsider f = NAT --> (0. V) as Function of NAT ,the carrier of V ;
let F be FinSequence of the carrier of V; :: thesis:
assume A24: len F = 0 ; :: thesis:
take u = f . (len F); :: thesis:
take f' = f; :: thesis:
thus ( u = f' . (len F) & f' . 0 = 0. V ) by FUNCOP_1:13; :: thesis:
let j be Element of NAT ; :: thesis:
thus for v being Element of V st j < len F & v = F . (j + 1) holds
f' . (j + 1) = (f' . j) + v by A24; :: thesis:

end;

then A25: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A25, A23);
hence ex b₁ being Element of V ex f being Function of NAT ,the carrier of V st
( b₁ = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) ; :: thesis: