:: deftheorem Def4 defines disjointify DYNKIN:def 4 :
for Omega being non empty set
for g, b₃ being SetSequence of Omega holds
( b₃ = disjointify g iff for n being Nat holds b₃ . n = disjointify (g,n) );