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 by FUNCT_2:def 1;
A2: dom (disjointify f) = NAT by FUNCT_2:def 1;
now :: thesis: for x being object st x in union (rng f) holds
x in union (rng (disjointify f))
let x be object ; :: thesis: ( x in union (rng f) implies x in union (rng (disjointify f)) )
defpred S1[ Nat] means x in f . $1;
assume x in union (rng f) ; :: thesis: x in union (rng (disjointify f))
then consider y being set such that
A3: x in y and
A4: y in rng f by TARSKI:def 4;
consider z being object such that
A5: z in dom f and
A6: y = f . z by A4, FUNCT_1:def 3;
reconsider n = z as Element of NAT by A5, FUNCT_2:def 1;
A7: ex k being Nat st S1[k]
proof
take n ; :: thesis: S1[n]
thus S1[n] by A3, A6; :: thesis: verum
end;
consider k being Nat such that
A8: ( S1[k] & ( for m being Nat st S1[m] holds
k <= m ) ) from NAT_1:sch 5(A7);
now :: thesis: not x in union (rng (f | k))
assume x in union (rng (f | k)) ; :: thesis: contradiction
then consider y being set such that
A9: x in y and
A10: y in rng (f | k) by TARSKI:def 4;
consider z being object such that
A11: z in dom (f | k) and
A12: y = (f | k) . z by A10, FUNCT_1:def 3;
dom (f | k) c= NAT by A1, RELAT_1:60;
then reconsider n = z as Element of NAT by A11;
dom (f | k) c= Segm k by RELAT_1:58;
then ( n < k & y = f . n ) by A11, A12, FUNCT_1:49, NAT_1:44;
hence contradiction by A8, A9; :: thesis: verum
end;
then x in (f . k) \ (union (rng (f | k))) by A8, XBOOLE_0:def 5;
then A13: x in (disjointify f) . k by Th4;
k in NAT by ORDINAL1:def 12;
then (disjointify f) . k in rng (disjointify f) by A2, FUNCT_1:def 3;
hence x in union (rng (disjointify f)) by A13, TARSKI:def 4; :: thesis: verum
end;
then A14: union (rng f) c= union (rng (disjointify f)) ;
now :: thesis: for x being object st x in union (rng (disjointify f)) holds
x in union (rng f)
let x be object ; :: 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
A15: x in y and
A16: y in rng (disjointify f) by TARSKI:def 4;
consider z being object such that
A17: z in dom (disjointify f) and
A18: y = (disjointify f) . z by A16, FUNCT_1:def 3;
reconsider n = z as Element of NAT by A17, FUNCT_2:def 1;
A19: ( (f . n) \ (union (rng (f | n))) c= f . n & f . n in rng f ) by A1, FUNCT_1:def 3, XBOOLE_1:36;
x in (f . n) \ (union (rng (f | n))) by A15, A18, Th4;
hence x in union (rng f) by A19, TARSKI:def 4; :: thesis: verum
end;
then union (rng (disjointify f)) c= union (rng f) ;
hence union (rng (disjointify f)) = union (rng f) by A14, XBOOLE_0:def 10; :: thesis: verum