theorem Th1: :: MEASURE4:1

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