let Omega be non empty set ; :: thesis: for f being SetSequence of Omega holds union (rng (disjointify f)) = union (rng f)
let f be SetSequence of Omega; :: thesis: union (rng (disjointify f)) = union (rng f)
A1: ( dom f = NAT & dom (disjointify f) = NAT ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in union (rng (disjointify f)) implies x in union (rng f) )
assume x in union (rng (disjointify f)) ; :: thesis: x in union (rng f)
then consider y being set such that
A2: ( x in y & y in rng (disjointify f) ) by TARSKI:def 4;
consider z being set such that
A3: ( z in dom (disjointify f) & y = (disjointify f) . z ) by A2, FUNCT_1:def 5;
reconsider n = z as Element of NAT by A3, FUNCT_2:def 1;
A4: x in (f . n) \ (union (rng (f | n))) by A2, A3, Th8;
A5: (f . n) \ (union (rng (f | n))) c= f . n by XBOOLE_1:36;
f . n in rng f by A1, FUNCT_1:def 5;
hence x in union (rng f) by A4, A5, TARSKI:def 4; :: thesis: verum

end;

then A6: union (rng (disjointify f)) c= union (rng f) by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in union (rng f) implies x in union (rng (disjointify f)) )
assume x in union (rng f) ; :: thesis: x in union (rng (disjointify f))
then consider y being set such that
A7: ( x in y & y in rng f ) by TARSKI:def 4;
consider z being set such that
A8: ( z in dom f & y = f . z ) by A7, FUNCT_1:def 5;
reconsider n = z as Element of NAT by A8, FUNCT_2:def 1;
defpred S₁[ Nat] means x in f . $1;
A9: ex k being Nat st S₁[k]

proof

take n ; :: thesis: S₁[n]
thus S₁[n] by A7, A8; :: thesis: verum

end;

consider k being Nat such that
A10: ( S₁[k] & ( for m being Nat st S₁[m] holds
k <= m ) ) from NAT_1:sch 5(A9);

now

assume x in union (rng (f | k)) ; :: thesis: contradiction
then consider y being set such that
A11: ( x in y & y in rng (f | k) ) by TARSKI:def 4;
consider z being set such that
A12: ( z in dom (f | k) & y = (f | k) . z ) by A11, FUNCT_1:def 5;
dom (f | k) c= NAT by A1, RELAT_1:89;
then reconsider n = z as Element of NAT by A12;
A13: dom (f | k) c= k by RELAT_1:87;
then A14: n < k by A12, NAT_1:45;
y = f . n by A12, A13, FUNCT_1:72;
hence contradiction by A10, A11, A14; :: thesis: verum

end;

then x in (f . k) \ (union (rng (f | k))) by A10, XBOOLE_0:def 5;
then A15: x in (disjointify f) . k by Th8;
k in NAT by ORDINAL1:def 13;
then (disjointify f) . k in rng (disjointify f) by A1, FUNCT_1:def 5;
hence x in union (rng (disjointify f)) by A15, TARSKI:def 4; :: thesis: verum

end;

then union (rng f) c= union (rng (disjointify f)) by TARSKI:def 3;
hence union (rng (disjointify f)) = union (rng f) by A6, XBOOLE_0:def 10; :: thesis: verum