per cases ( not I is empty or I is empty ) ;

suppose A1: not I is empty ; :: thesis: ex b₁ being set st
for x being set holds
( x in b₁ iff x is ManySortedSubset of M )

consider X being set such that
A2: for e being set holds
( e in X iff ( e in Funcs (I,(union (rng (bool M)))) & S₁[e] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being set holds
( x in X iff x is ManySortedSubset of M )
thus for x being set holds
( x in X iff x is ManySortedSubset of M ) :: thesis: verum

proof

let x be set ; :: thesis: ( x in X iff x is ManySortedSubset of M )
thus ( x in X implies x is ManySortedSubset of M ) by A2; :: thesis: ( x is ManySortedSubset of M implies x in X )
assume A3: x is ManySortedSubset of M ; :: thesis: x in X

now :: thesis: ( x in Funcs (I,(union (rng (bool M)))) & S₁[x] )

reconsider xx = x as ManySortedSubset of M by A3;
( dom xx = I & rng xx c= union (rng (bool M)) ) by A1, Th2, PARTFUN1:def 2;
hence x in Funcs (I,(union (rng (bool M)))) by FUNCT_2:def 2; :: thesis: S₁[x]
thus S₁[x] by A3; :: thesis: verum

end;

hence x in X by A2; :: thesis: verum

end;

end;

suppose A4: I is empty ; :: thesis: ex b₁ being set st
for x being set holds
( x in b₁ iff x is ManySortedSubset of M )

take {([[0]] {})} ; :: thesis: for x being set holds
( x in {([[0]] {})} iff x is ManySortedSubset of M )
thus for x being set holds
( x in {([[0]] {})} iff x is ManySortedSubset of M ) :: thesis: verum

proof

let x be set ; :: thesis: ( x in {([[0]] {})} iff x is ManySortedSubset of M )
thus ( x in {([[0]] {})} implies x is ManySortedSubset of M ) :: thesis: ( x is ManySortedSubset of M implies x in {([[0]] {})} )

proof

reconsider M9 = M as ManySortedSet of {} by A4;
assume A6: x in {([[0]] {})} ; :: thesis: x is ManySortedSubset of M
reconsider y = [[0]] {} as ManySortedSubset of M9 by PBOOLE:def 18;
y is ManySortedSubset of M by A4;
hence x is ManySortedSubset of M by A6, TARSKI:def 1; :: thesis: verum

end;

assume x is ManySortedSubset of M ; :: thesis: x in {([[0]] {})}
then consider y being ManySortedSubset of M such that
A7: y = x ;
y = [[0]] {} by A4;
hence x in {([[0]] {})} by A7, TARSKI:def 1; :: thesis: verum

end;

end;

end;