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 :: thesis: for x being object st x in Segm (n + 1) holds
b1 . x = b2 . x

let x be object ; :: thesis: ( x in Segm (n + 1) implies b1 . b₁ = b2 . b₁ )
assume A14: x in Segm (n + 1) ; :: thesis: b1 . b₁ = b2 . b₁
then A15: x in (Segm n) \/ {n} by AFINSQ_1:2;

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