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

A13: now :: thesis:

let x be object ; :: thesis:
assume A14: x in Segm (n + 1) ; :: thesis:
then A15: x in (Segm n) \/ {n} by AFINSQ_1:2;

suppose x in {n} ; :: thesis:

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

end;

suppose not x in {n} ; :: thesis:

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:

end;

end;

end;

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