let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S st M is sigma_finite holds
COM M is sigma_finite
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S st M is sigma_finite holds
COM M is sigma_finite
let M be sigma_Measure of S; :: thesis: ( M is sigma_finite implies COM M is sigma_finite )
assume M is sigma_finite ; :: thesis: COM M is sigma_finite
then consider E being Set_Sequence of S such that
A1: for n being Nat holds M . (E . n) < +infty and
A2: Union E = X by MEASUR11:def 12;
for n being Nat holds E . n in COM (S,M)

proof

let n be Nat; :: thesis: E . n in COM (S,M)
E . n is Element of COM (S,M) by MESFUN14:27;
hence E . n in COM (S,M) ; :: thesis: verum

end;

then reconsider E1 = E as Set_Sequence of COM (S,M) by MEASURE8:def 2;
for n being Nat holds (COM M) . (E1 . n) < +infty

proof

let n be Nat; :: thesis: (COM M) . (E1 . n) < +infty
M . (E . n) < +infty by A1;
hence (COM M) . (E1 . n) < +infty by MESFUN14:35; :: thesis: verum

end;

hence COM M is sigma_finite by A2, MEASUR11:def 12; :: thesis: verum