defpred S₁[ set ] means for F being Bags I -valued FinSequence st len F = $1 holds
ex u being bag of I ex f being Function of NAT,(Bags I) st
( u = f . (len F) & f . 0 = EmptyBag I & ( for j being Nat
for v being bag of I st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) );
set V = Bags I;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A2: S₁[n] ; :: thesis:
let F be Bags I -valued FinSequence; :: thesis:
A3: rng F c= Bags I by RELAT_1:def 19;
then reconsider F1 = F as FinSequence of Bags I by FINSEQ_1:def 4;
reconsider G = F1 | (Seg n) as FinSequence of Bags I by FINSEQ_1:18;
assume A4: 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 Bags I by A3;
A5: n < n + 1 by NAT_1:13;
then consider u being bag of I, f being Function of NAT,(Bags I) such that
u = f . (len G) and
A6: f . 0 = EmptyBag I and
A7: for j being Nat
for v being bag of I st j < len G & v = G . (j + 1) holds
f . (j + 1) = (f . j) + v by A2, A4, FINSEQ_1:17;
defpred S₂[ set , set ] means for j being Nat st $1 = j holds
( ( j < n + 1 implies $2 = f . $1 ) & ( n + 1 <= j implies for u being bag of I st u = F . (n + 1) holds
$2 = (f . (len G)) + u ) );
A8: for k being Element of NAT ex v being Element of Bags I st S₂[k,v]

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

assume A10: n + 1 <= i ; :: thesis:
take v = (f . (len G)) + u1; :: thesis:
let j be Nat; :: thesis:
assume k = j ; :: thesis:
hence ( j < n + 1 implies v = f . k ) by A10; :: thesis:
assume n + 1 <= j ; :: thesis:
let u2 be bag of I; :: thesis:
assume u2 = F . (n + 1) ; :: thesis:
hence v = (f . (len G)) + u2 ; :: thesis:

end;

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

end;

then consider v being bag of I such that
B13: S₂[k,v] by A9;
v in Bags I by PRE_POLY:def 12;
hence ex v being Element of Bags I st S₂[k,v] by B13; :: thesis:

end;

consider f9 being sequence of (Bags I) such that
A13: for k being Element of NAT holds S₂[k,f9 . k] from FUNCT_2:sch 3(A8);
A14: for k being Nat holds S₂[k,f9 . k]

end;

take z = f9 . (n + 1); :: thesis:
take f99 = f9; :: thesis:
thus z = f99 . (len F) by A4; :: thesis:
thus f99 . 0 = EmptyBag I by A6, A14; :: thesis:
let j be Nat; :: thesis:
let v be bag of I; :: thesis:
assume that
A15: j < len F and
A16: v = F . (j + 1) ; :: thesis:
A17: len G = n by A4, A5, FINSEQ_1:17;

assume A19: j = n ; :: thesis:
then f99 . (j + 1) = (f . j) + v by A17, A14, A16;
hence f99 . (j + 1) = (f99 . j) + v by A5, A14, A19; :: thesis:

end;

end;

j <= n by A4, A15, NAT_1:13;
hence f99 . (j + 1) = (f99 . j) + v by A20, A18, XXREAL_0:1; :: thesis:

end;

reconsider f = NAT --> (EmptyBag I) as sequence of (Bags I) ;
let F be Bags I -valued FinSequence; :: thesis:
assume A26: len F = 0 ; :: thesis:
take u = f . (len F); :: thesis:
take f9 = f; :: thesis:
thus ( u = f9 . (len F) & f9 . 0 = EmptyBag I ) by FUNCOP_1:7; :: thesis:
let j be Nat; :: thesis:
let v be bag of I; :: thesis:
thus ( j < len F & v = F . (j + 1) implies f9 . (j + 1) = (f9 . j) + v ) by A26; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A25, A1);
hence ex b₁ being bag of I ex F being Function of NAT,(Bags I) st
( b₁ = F . (len f) & F . 0 = EmptyBag I & ( for i being Nat
for b being bag of I st i < len f & b = f . (i + 1) holds
F . (i + 1) = (F . i) + b ) ) ; :: thesis: