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;
A5: union (rng (f | n)) in D by A1, A2, A4, Th14, 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, Th12;
hence (disjointify f) . n in D by Th4; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (disjointify f) or y in D )
assume y in rng (disjointify f) ; :: thesis: y in D
then consider x being object 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