theorem Th4: :: DYNKIN:5

for Omega being non empty set
for f being SetSequence of Omega
for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n)))