let X be set ; :: thesis: for C being C_Measure of X
for seq being SetSequence of sigma_Field C holds Union seq in sigma_Field C
let C be C_Measure of X; :: thesis: for seq being SetSequence of sigma_Field C holds Union seq in sigma_Field C
let seq be SetSequence of sigma_Field C; :: thesis: Union seq in sigma_Field C
set Aseq = Partial_Diff_Union seq;
rng (Partial_Diff_Union seq) c= sigma_Field C by RELAT_1:def 19;
then reconsider Aseq9 = Partial_Diff_Union seq as sequence of (sigma_Field C) by FUNCT_2:6;
reconsider Aseq9 = Aseq9 as Sep_Sequence of (sigma_Field C) ;
union (rng Aseq9) in sigma_Field C by Th24;
then Union (Partial_Diff_Union seq) in sigma_Field C by CARD_3:def 4;
hence Union seq in sigma_Field C by PROB_3:36; :: thesis: verum