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:def 9 ;
:: thesis: verum