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;

hence b1 = b2 by A12, A13, FUNCT_1:2; :: thesis: verum

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

dom b2 = n + 1
by PARTFUN1:def 2;b1 . x = b2 . x

let x be object ; :: thesis: ( x in Segm (n + 1) implies b1 . b_{1} = b2 . b_{1} )

assume A14: x in Segm (n + 1) ; :: thesis: b1 . b_{1} = b2 . b_{1}

then A15: x in (Segm n) \/ {n} by AFINSQ_1:2;

end;assume A14: x in Segm (n + 1) ; :: thesis: b1 . b

then A15: x in (Segm n) \/ {n} by AFINSQ_1:2;

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

end;

suppose
not x in {n}
; :: thesis: b1 . b_{1} = b2 . b_{1}

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;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

hence b1 = b2 by A12, A13, FUNCT_1:2; :: thesis: verum