let b3, b4 be bag of X; :: thesis: ( ( for k being object holds b3 . k = max ((b1 . k),(b2 . k)) ) & ( for k being object holds b4 . k = max ((b1 . k),(b2 . k)) ) implies b3 = b4 )

assume A13: for k being object holds b3 . k = max ((b1 . k),(b2 . k)) ; :: thesis: ( ex k being object st not b4 . k = max ((b1 . k),(b2 . k)) or b3 = b4 )

assume A14: for k being object holds b4 . k = max ((b1 . k),(b2 . k)) ; :: thesis: b3 = b4

.= dom b4 by PARTFUN1:def 2 ;

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

assume A13: for k being object holds b3 . k = max ((b1 . k),(b2 . k)) ; :: thesis: ( ex k being object st not b4 . k = max ((b1 . k),(b2 . k)) or b3 = b4 )

assume A14: for k being object holds b4 . k = max ((b1 . k),(b2 . k)) ; :: thesis: b3 = b4

A15: now :: thesis: for u being object st u in dom b3 holds

b3 . u = b4 . u

dom b3 =
X
by PARTFUN1:def 2
b3 . u = b4 . u

let u be object ; :: thesis: ( u in dom b3 implies b3 . u = b4 . u )

assume u in dom b3 ; :: thesis: b3 . u = b4 . u

thus b3 . u = max ((b1 . u),(b2 . u)) by A13

.= b4 . u by A14 ; :: thesis: verum

end;assume u in dom b3 ; :: thesis: b3 . u = b4 . u

thus b3 . u = max ((b1 . u),(b2 . u)) by A13

.= b4 . u by A14 ; :: thesis: verum

.= dom b4 by PARTFUN1:def 2 ;

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