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:70;
( dom (f | n) c= Segm n & rng f is Subset-Family of Omega ) by RELAT_1:58, RELAT_1:def 19;
then rng (f | n) is finite Subset-Family of Omega by A4, XBOOLE_1:1;
then A5: union (rng (f | n)) in D by A1, A2, A4, Th18, XBOOLE_1:1;
then reconsider urf = union (rng (f | n)) as Subset of Omega ;
dom f = NAT by FUNCT_2:def 1;
then f . n in rng f by FUNCT_1:def 3;
then (f . n) \ urf in D by A1, A2, A5, 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
A6: x in dom (disjointify f) and
A7: y = (disjointify f) . x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A6, FUNCT_2:def 1;
y = (disjointify f) . n by A7;
hence y in D by A3; :: thesis: verum

end;

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