M is ManySortedSubset of M by PBOOLE:def 18;
hence not Bool M is empty by Def1; :: thesis: ( Bool M is functional & Bool M is with_common_domain )
thus Bool M is functional :: thesis: Bool M is with_common_domain

proof

let x be set ; :: according to FUNCT_1:def 13 :: thesis: ( not x in Bool M or x is set )
assume x in Bool M ; :: thesis: x is set
hence x is set 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 proj1 f = proj1 g )
assume that
A1: f in Bool M and
A2: g in Bool M ; :: thesis: proj1 f = proj1 g
A3: g is ManySortedSubset of M by A2, Def1;
f is ManySortedSubset of M by A1, Def1;
hence dom f = I by PARTFUN1:def 2
.= dom g by A3, PARTFUN1:def 2 ;
:: thesis: verum