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 Function of NAT,(sigma_Field C) by FUNCT_2:8;
reconsider Aseq9 = Aseq9 as Sep_Sequence of (sigma_Field C) by PROB_3:41;
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:40; :: thesis: verum