let b1, b2 be bag of n; :: thesis: ( ( for i being Nat st i in n holds
b1 . i = card (f " {(i + 1)}) ) & ( for i being Nat st i in n holds
b2 . i = card (f " {(i + 1)}) ) implies b1 = b2 )
assume that
A4: for i being Nat st i in n holds
b1 . i = card (f " {(i + 1)}) and
A5: for i being Nat st i in n holds
b2 . i = card (f " {(i + 1)}) ; :: thesis: b1 = b2
A6: ( dom b1 = n & n = dom b2 ) by PARTFUN1:def 2;
for x being object st x in dom b1 holds
b1 . x = b2 . x

proof

let x be object ; :: thesis: ( x in dom b1 implies b1 . x = b2 . x )
assume A7: x in dom b1 ; :: thesis: b1 . x = b2 . x
x in Segm n by A7;
then reconsider i = x as Nat ;
thus b1 . x = card (f " {(i + 1)}) by A7, A4
.= b2 . x by A5, A7 ; :: thesis: verum

end;

hence b1 = b2 by A6; :: thesis: verum