let I be set ; :: thesis: for A, B being ManySortedSet of I holds union (A (/\) B) c= (union A) (/\) (union B)
let A, B be ManySortedSet of I; :: thesis: union (A (/\) B) c= (union A) (/\) (union B)
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or (union (A (/\) B)) . i c= ((union A) (/\) (union B)) . i )
assume A1: i in I ; :: thesis: (union (A (/\) B)) . i c= ((union A) (/\) (union B)) . i
then A2: (union (A (/\) B)) . i = union ((A . i) /\ (B . i)) by Lm7;
((union A) (/\) (union B)) . i = ((union A) . i) /\ ((union B) . i) by A1, PBOOLE:def 5
.= (union (A . i)) /\ ((union B) . i) by A1, Def2
.= (union (A . i)) /\ (union (B . i)) by A1, Def2 ;
hence (union (A (/\) B)) . i c= ((union A) (/\) (union B)) . i by A2, ZFMISC_1:79; :: thesis: verum