let I be set ; :: thesis: for M being ManySortedSet of holds |:(Bool M):| = bool M
let M be ManySortedSet of ; :: thesis: |:(Bool M):| = bool M

now

let i be set ; :: thesis: ( i in I implies |:(Bool M):| . i = (bool M) . i )
assume A1: i in I ; :: thesis: |:(Bool M):| . i = (bool M) . i
then A2: |:(Bool M):| . i = { (x . i) where x is Element of Bool M : x in Bool M } by Th15;
thus |:(Bool M):| . i = (bool M) . i :: thesis: verum

proof

thus |:(Bool M):| . i c= (bool M) . i :: according to XBOOLE_0:def 10 :: thesis: (bool M) . i c= |:(Bool M):| . i

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in |:(Bool M):| . i or q in (bool M) . i )
assume q in |:(Bool M):| . i ; :: thesis: q in (bool M) . i
then consider x being Element of Bool M such that
A3: q = x . i and
x in Bool M by A2;
x c= M by PBOOLE:def 23;
then x . i c= M . i by A1, PBOOLE:def 5;
then x . i in bool (M . i) ;
hence q in (bool M) . i by A1, A3, MBOOLEAN:def 1; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (bool M) . i or a in |:(Bool M):| . i )
assume A4: a in (bool M) . i ; :: thesis: a in |:(Bool M):| . i
dom (([0] I) +* (i .--> a)) = I by A1, PZFMISC1:1;
then reconsider X = ([0] I) +* (i .--> a) as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
A5: dom (i .--> a) = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A6: X . i = (i .--> a) . i by A5, FUNCT_4:14
.= a by FUNCOP_1:87 ;
X is ManySortedSubset of M

proof

let s be set ; :: according to PBOOLE:def 5,PBOOLE:def 23 :: thesis: ( not s in I or X . s c= M . s )
assume A7: s in I ; :: thesis: X . s c= M . s

per cases ( s = i or s <> i ) ;

suppose A8: s = i ; :: thesis: X . s c= M . s

then a in bool (M . s) by A4, A7, MBOOLEAN:def 1;
hence X . s c= M . s by A6, A8; :: thesis: verum

end;

suppose s <> i ; :: thesis: X . s c= M . s

then not s in dom (i .--> a) by A5, TARSKI:def 1;
then X . s = ([0] I) . s by FUNCT_4:12
.= {} by PBOOLE:5 ;
hence X . s c= M . s by XBOOLE_1:2; :: thesis: verum

end;

end;

end;

then X is Element of Bool M by Def1;
then consider x being Element of Bool M such that
A9: a = x . i by A6;
thus a in |:(Bool M):| . i by A2, A9; :: thesis: verum

end;

end;

hence |:(Bool M):| = bool M by PBOOLE:3; :: thesis: verum