let I be set ; :: thesis: for A, B being ManySortedSet of st A c= B holds
bool A c= bool B
let A, B be ManySortedSet of ; :: thesis: ( A c= B implies bool A c= bool B )
assume A1: A c= B ; :: thesis: bool A c= bool B
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or (bool A) . i c= (bool B) . i )
assume A2: i in I ; :: thesis: (bool A) . i c= (bool B) . i
then A3: ( (bool A) . i = bool (A . i) & (bool B) . i = bool (B . i) ) by Def1;
A . i c= B . i by A1, A2, PBOOLE:def 5;
hence (bool A) . i c= (bool B) . i by A3, ZFMISC_1:79; :: thesis: verum