let I be set ; :: thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(union (A (/\) B)) . i = union ((A . i) /\ (B . i))
let A, B be ManySortedSet of I; :: thesis: for i being set st i in I holds
(union (A (/\) B)) . i = union ((A . i) /\ (B . i))
let i be set ; :: thesis: ( i in I implies (union (A (/\) B)) . i = union ((A . i) /\ (B . i)) )
assume A1: i in I ; :: thesis: (union (A (/\) B)) . i = union ((A . i) /\ (B . i))
hence (union (A (/\) B)) . i = union ((A (/\) B) . i) by Def2
.= union ((A . i) /\ (B . i)) by A1, PBOOLE:def 5 ;
:: thesis: verum