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

A15: now :: thesis: for u being object st u in dom b3 holds
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;

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