for X being non empty set
for F being Field_Subset of X
for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st
( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds
for M being sigma_Measure of (sigma F) st M is_extension_of m holds
M = (sigma_Meas (C_Meas m)) | (sigma F)