let v1, v2 be bag of I; :: thesis: ( ex F being Function of NAT,(Bags I) st
( v1 = 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 ) ) & ex F being Function of NAT,(Bags I) st
( v2 = 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 ) ) implies v1 = v2 )
given F being Function of NAT,(Bags I) such that A27: v1 = F . (len f) and
A28: F . 0 = EmptyBag I and
A29: 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 ; :: thesis: ( for F being Function of NAT,(Bags I) holds
( not v2 = F . (len f) or not F . 0 = EmptyBag I or ex i being Nat ex b being bag of I st
( i < len f & b = f . (i + 1) & not F . (i + 1) = (F . i) + b ) ) or v1 = v2 )
given f9 being Function of NAT,(Bags I) such that A30: v2 = f9 . (len f) and
A31: f9 . 0 = EmptyBag I and
A32: for j being Nat
for v being bag of I st j < len f & v = f . (j + 1) holds
f9 . (j + 1) = (f9 . j) + v ; :: thesis: v1 = v2
defpred S₁[ Nat] means ( $1 <= len f implies F . $1 = f9 . $1 );

now :: thesis: for k being Nat st S₁[k] & k + 1 <= len f holds
F . (k + 1) = f9 . (k + 1)

A33: rng f c= Bags I by RELAT_1:def 19;
let k be Nat; :: thesis: ( S₁[k] & k + 1 <= len f implies F . (k + 1) = f9 . (k + 1) )
assume A34: S₁[k] ; :: thesis: ( k + 1 <= len f implies F . (k + 1) = f9 . (k + 1) )
assume A35: k + 1 <= len f ; :: thesis: F . (k + 1) = f9 . (k + 1)
( 1 <= k + 1 & dom f = Seg (len f) ) by FINSEQ_1:def 3, NAT_1:11;
then k + 1 in dom f by A35;
then f . (k + 1) in rng f by FUNCT_1:def 3;
then reconsider u1 = f . (k + 1) as Element of Bags I by A33;
F . (k + 1) = (F . k) + u1 by A29, A35, NAT_1:13;
hence F . (k + 1) = f9 . (k + 1) by A32, A34, A35, NAT_1:13; :: thesis: verum

end;

then A37: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A38: S₁[ 0 ] by A28, A31;
for k being Nat holds S₁[k] from NAT_1:sch 2(A38, A37);
hence v1 = v2 by A27, A30; :: thesis: verum