defpred S₁[ set ] means for F being the carrier of V -valued FinSequence st len F = $1 holds
ex u being Element of V ex f being Function of NAT,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 ) );
A23: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

let n be Element of NAT ; :: thesis:
assume A1: for F being the carrier of V -valued FinSequence st len F = n holds
ex u being Element of V ex f being Function of NAT,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 the carrier of V -valued FinSequence; :: thesis:
A2: rng F c= the carrier of V by RELAT_1:def 19;
then reconsider F1 = F as FinSequence of V by FINSEQ_1:def 4;
reconsider G = F1 | (Seg n) as FinSequence of V by FINSEQ_1:18;
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:4;
then F . (n + 1) in rng F by FUNCT_1:def 3;
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,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:17;
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 ;

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;

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;

end;

consider f9 being Function of NAT, the carrier of V such that
A12: for k being Element of NAT holds S₂[k,f9 . k] from FUNCT_2:sch 3(A7);
take z = f9 . (n + 1); :: thesis:
take f99 = f9; :: thesis:
thus z = f99 . (len F) by A3; :: thesis:
thus f99 . 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:17;

A16: now

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

end;

A18: now

end;

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

end;

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

end;

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,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: