thus not Bool M is empty :: thesis: ( Bool M is functional & Bool M is with_common_domain )

proof

M is ManySortedSubset of M

proof

thus M c= M ; :: according to PBOOLE:def 23 :: thesis: verum

end;

hence not Bool M is empty by Def1; :: thesis: verum

end;

thus Bool M is functional :: thesis: Bool M is with_common_domain

proof

let x be set ; :: according to FRAENKEL:def 1 :: thesis: ( not x in Bool M or x is set )
assume x in Bool M ; :: thesis: x is set
hence x is Function by Def1; :: thesis: verum

end;

let f, g be Function; :: according to CARD_3:def 10 :: thesis: ( not f in Bool M or not g in Bool M or dom f = dom g )
assume ( f in Bool M & g in Bool M ) ; :: thesis: dom f = dom g
then A1: ( f is ManySortedSubset of M & g is ManySortedSubset of M ) by Def1;
hence dom f = I by PBOOLE:def 3
.= dom g by A1, PBOOLE:def 3 ;
:: thesis: verum