let I be set ; :: thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A (\+\) B)) . i = bool ((A . i) \+\ (B . i))
let A, B be ManySortedSet of I; :: thesis: for i being set st i in I holds
(bool (A (\+\) B)) . i = bool ((A . i) \+\ (B . i))
let i be set ; :: thesis: ( i in I implies (bool (A (\+\) B)) . i = bool ((A . i) \+\ (B . i)) )
assume A1: i in I ; :: thesis: (bool (A (\+\) B)) . i = bool ((A . i) \+\ (B . i))
hence (bool (A (\+\) B)) . i = bool ((A (\+\) B) . i) by Def1
.= bool ((A . i) \+\ (B . i)) by A1, PBOOLE:4 ;
:: thesis: verum