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

.= dom b4 by PARTFUN1:def 2 ;

hence b3 = b4 by A4, FUNCT_1:2; :: thesis: verum

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

dom b3 =
X
by PARTFUN1:def 2
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;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

.= dom b4 by PARTFUN1:def 2 ;

hence b3 = b4 by A4, FUNCT_1:2; :: thesis: verum