theorem Th6: :: MESFUNC3:6

for X being non empty set
for A being set
for F, G being FinSequence of X st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
union (rng G) = A /\ (union (rng F))