let b3, b4 be bag of ; :: 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 A13: 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 A14: for k being set holds b4 . k = max (b1 . k),(b2 . k) ; :: thesis: b3 = b4
A15: dom b3 = X by PARTFUN1:def 4
.= dom b4 by PARTFUN1:def 4 ;

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 A13
.= b4 . u by A14 ; :: thesis: verum

end;

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