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 4
.= dom b4 by PARTFUN1:def 4 ;
hence b3 = b4 by A16, FUNCT_1:9; :: thesis: verum