let b1, b2 be Element of Bags (n + 1); :: thesis: ( b1 | n = b & b1 . n = k & b2 | n = b & b2 . n = k implies b1 = b2 )
assume that
A8: b1 | n = b and
A9: b1 . n = k and
A10: b2 | n = b and
A11: b2 . n = k ; :: thesis: b1 = b2
A12: dom b1 = n + 1 by PARTFUN1:def 2;

A13: now

let x be set ; :: thesis: ( x in n + 1 implies b1 . b₁ = b2 . b₁ )
assume A14: x in n + 1 ; :: thesis: b1 . b₁ = b2 . b₁
then x in succ n by NAT_1:38;
then A15: x in n \/ {n} by ORDINAL1:def 1;

per cases ( x in {n} or not x in {n} ) ;

suppose x in {n} ; :: thesis: b1 . b₁ = b2 . b₁

then x = n by TARSKI:def 1;
hence b1 . x = b2 . x by A9, A11; :: thesis: verum

end;

suppose not x in {n} ; :: thesis: b1 . b₁ = b2 . b₁

then x in n by A15, XBOOLE_0:def 3;
then x in (n + 1) /\ n by A14, XBOOLE_0:def 4;
then A16: x in dom b by A8, A12, RELAT_1:61;
hence b1 . x = b . x by A8, FUNCT_1:47
.= b2 . x by A10, A16, FUNCT_1:47 ;
:: thesis: verum

end;

end;

end;

dom b2 = n + 1 by PARTFUN1:def 2;
hence b1 = b2 by A12, A13, FUNCT_1:2; :: thesis: verum