let Omega be non empty set ; :: thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D
let D be non empty Subset-Family of Omega; :: thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D )
assume A1: ( D is Dynkin_System of Omega & D is intersection_stable ) ; :: thesis: for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D
let f be SetSequence of Omega; :: thesis: ( rng f c= D implies rng (disjointify f) c= D )
assume A2: rng f c= D ; :: thesis: rng (disjointify f) c= D
A3: for n being Element of NAT holds (disjointify f) . n in D

proof

let n be Element of NAT ; :: thesis: (disjointify f) . n in D
A4: rng (f | n) c= rng f by RELAT_1:99;
A5: dom (f | n) c= Segm n by RELAT_1:87;
rng f is Subset-Family of Omega by RELAT_1:def 19;
then rng (f | n) is finite Subset-Family of Omega by A4, A5, FINSET_1:26, XBOOLE_1:1;
then A6: union (rng (f | n)) in D by A1, A2, A4, Th18, XBOOLE_1:1;
dom f = NAT by FUNCT_2:def 1;
then A7: f . n in rng f by FUNCT_1:def 5;
reconsider urf = union (rng (f | n)) as Subset of Omega by A6;
(f . n) \ urf in D by A1, A2, A6, A7, Th16;
hence (disjointify f) . n in D by Th8; :: thesis: verum

end;

now

let y be set ; :: thesis: ( y in rng (disjointify f) implies y in D )
assume y in rng (disjointify f) ; :: thesis: y in D
then consider x being set such that
A8: ( x in dom (disjointify f) & y = (disjointify f) . x ) by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A8, FUNCT_2:def 1;
y = (disjointify f) . n by A8;
hence y in D by A3; :: thesis: verum

end;

hence rng (disjointify f) c= D by TARSKI:def 3; :: thesis: verum