let b3, b4 be bag of X; :: thesis: ( ( for k being set holds b3 . k = max ((b1 . k),(b2 . k)) ) & ( for k being set holds b4 . k = max ((b1 . k),(b2 . k)) ) implies b3 = b4 )
assume A14: for k being set holds b3 . k = max ((b1 . k),(b2 . k)) ; :: thesis: ( ex k being set st not b4 . k = max ((b1 . k),(b2 . k)) or b3 = b4 )
assume A15: for k being set holds b4 . k = max ((b1 . k),(b2 . k)) ; :: thesis: b3 = b4

A16: now

let u be set ; :: 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 A14
.= b4 . u by A15 ; :: thesis: verum

end;

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