let I be set ; :: thesis: for A, B being ManySortedSet of holds union (A /\ B) c= (union A) /\ (union B)
let A, B be ManySortedSet of ; :: thesis: union (A /\ B) c= (union A) /\ (union B)
let i be set ; :: according to PBOOLE:def 5 :: 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 8
.= (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:97; :: thesis: verum