let I be set ; :: thesis: for A, B being ManySortedSet of I holds bool (A (\) B) c= (I --> {{}}) (\/) ((bool A) (\) (bool B))
let A, B be ManySortedSet of I; :: thesis: bool (A (\) B) c= (I --> {{}}) (\/) ((bool A) (\) (bool B))
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or (bool (A (\) B)) . i c= ((I --> {{}}) (\/) ((bool A) (\) (bool B))) . i )
assume A1: i in I ; :: thesis: (bool (A (\) B)) . i c= ((I --> {{}}) (\/) ((bool A) (\) (bool B))) . i
then A2: (bool (A (\) B)) . i = bool ((A . i) \ (B . i)) by Lm4;
((I --> {{}}) (\/) ((bool A) (\) (bool B))) . i = ((I --> {{}}) . i) \/ (((bool A) (\) (bool B)) . i) by A1, PBOOLE:def 4
.= {{}} \/ (((bool A) (\) (bool B)) . i) by A1, FUNCOP_1:7
.= {{}} \/ (((bool A) . i) \ ((bool B) . i)) by A1, PBOOLE:def 6
.= {{}} \/ ((bool (A . i)) \ ((bool B) . i)) by A1, Def1
.= {{}} \/ ((bool (A . i)) \ (bool (B . i))) by A1, Def1 ;
hence (bool (A (\) B)) . i c= ((I --> {{}}) (\/) ((bool A) (\) (bool B))) . i by A2, ZFMISC_1:72; :: thesis: verum