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

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