theorem Th20: :: MEASURE2:20

for X being set
for S being SigmaField of X
for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
union (rng F) = union (rng N)