theorem Th20: :: MESFUN15:18

for X, Y being non empty set
for A being set
for F being sequence of X
for G being sequence of Y st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))