let I be set ; :: thesis: for M being ManySortedSet of I
for x being set holds
( x is ManySortedSubset of M iff x in product (bool M) )
let M be ManySortedSet of I; :: thesis: for x being set holds
( x is ManySortedSubset of M iff x in product (bool M) )
let x be set ; :: thesis: ( x is ManySortedSubset of M iff x in product (bool M) )
A1: I = dom (bool M) by PARTFUN1:def 2;

hereby :: thesis: ( x in product (bool M) implies x is ManySortedSubset of M )

assume x is ManySortedSubset of M ; :: thesis: x in product (bool M)
then reconsider x1 = x as ManySortedSubset of M ;
A2: for i being object st i in dom (bool M) holds
x1 . i in (bool M) . i

proof

let i be object ; :: thesis: ( i in dom (bool M) implies x1 . i in (bool M) . i )
assume A3: i in dom (bool M) ; :: thesis: x1 . i in (bool M) . i
x1 c= M by PBOOLE:def 18;
then x1 . i c= M . i by A1, A3;
then x1 . i in bool (M . i) ;
hence x1 . i in (bool M) . i by A1, A3, MBOOLEAN:def 1; :: thesis: verum

end;

dom x1 = I by PARTFUN1:def 2
.= dom (bool M) by PARTFUN1:def 2 ;
hence x in product (bool M) by A2, CARD_3:def 5; :: thesis: verum

end;

assume x in product (bool M) ; :: thesis: x is ManySortedSubset of M
then consider x1 being Function such that
A4: x = x1 and
A5: dom x1 = dom (bool M) and
A6: for i being object st i in dom (bool M) holds
x1 . i in (bool M) . i by CARD_3:def 5;
dom x1 = I by A5, PARTFUN1:def 2;
then reconsider x2 = x1 as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
x2 c= M

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or x2 . i c= M . i )
assume A7: i in I ; :: thesis: x2 . i c= M . i
x2 . i in (bool M) . i by A1, A6, A7;
then x2 . i in bool (M . i) by A7, MBOOLEAN:def 1;
hence x2 . i c= M . i ; :: thesis: verum

end;

hence x is ManySortedSubset of M by A4, PBOOLE:def 18; :: thesis: verum