let Omega be non empty set ; :: thesis: for f being SetSequence of Omega
for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n)))
let f be SetSequence of Omega; :: thesis: for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n)))
let n be Nat; :: thesis: (disjointify f) . n = (f . n) \ (union (rng (f | n)))
(disjointify f) . n = disjointify (f,n) by Def4;
hence (disjointify f) . n = (f . n) \ (union (rng (f | n))) ; :: thesis: verum