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

now :: thesis: for i being object st i in I holds
|:(Bool M):| . i = (bool M) . i

let i be object ; :: 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 Th14;
thus |:(Bool M):| . i = (bool M) . i :: thesis: verum

proof

thus |:(Bool M):| . i c= (bool M) . i by A1, PBOOLE:def 2, PBOOLE:def 18; :: according to XBOOLE_0:def 10 :: thesis: (bool M) . i c= |:(Bool M):| . i
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (bool M) . i or a in |:(Bool M):| . i )
assume A3: a in (bool M) . i ; :: thesis: a in |:(Bool M):| . i
dom ((EmptyMS I) +* (i .--> a)) = I by A1, PZFMISC1:1;
then reconsider X = (EmptyMS I) +* (i .--> a) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A4: dom (i .--> a) = {i} ;
i in {i} by TARSKI:def 1;
then A5: X . i = (i .--> a) . i by A4, FUNCT_4:13
.= a by FUNCOP_1:72 ;
X is ManySortedSubset of M

proof

let s be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not s in I or X . s c= M . s )
assume A6: s in I ; :: thesis: X . s c= M . s

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

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

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

end;

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

then not s in dom (i .--> a) by TARSKI:def 1;
then X . s = (EmptyMS I) . s by FUNCT_4:11
.= {} ;
hence X . s c= M . s ; :: thesis: verum

end;

end;

end;

then X is Element of Bool M by Def1;
hence a in |:(Bool M):| . i by A2, A5; :: thesis: verum

end;

end;

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