let b3, b4 be bag of X; :: thesis: ( b2 + b3 = b1 & b2 + b4 = b1 implies b3 = b4 )
assume A2: b2 + b3 = b1 ; :: thesis: ( not b2 + b4 = b1 or b3 = b4 )
assume A3: b2 + b4 = b1 ; :: thesis: b3 = b4

A4: now :: thesis: for x being object st x in dom b3 holds
b3 . x = b4 . x

let x be object ; :: thesis: ( x in dom b3 implies b3 . x = b4 . x )
assume x in dom b3 ; :: thesis: b3 . x = b4 . x
thus b3 . x = ((b2 . x) + (b3 . x)) -' (b2 . x) by NAT_D:34
.= (b1 . x) -' (b2 . x) by A2, PRE_POLY:def 5
.= ((b2 . x) + (b4 . x)) -' (b2 . x) by A3, PRE_POLY:def 5
.= b4 . x by NAT_D:34 ; :: thesis: verum

end;

dom b3 = X by PARTFUN1:def 2
.= dom b4 by PARTFUN1:def 2 ;
hence b3 = b4 by A4, FUNCT_1:2; :: thesis: verum