:: deftheorem defines disjointify DYNKIN:def 3 :
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)));