let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S holds E is Element of COM (S,M)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S holds E is Element of COM (S,M)
let M be sigma_Measure of S; :: thesis: for E being Element of S holds E is Element of COM (S,M)
let E be Element of S; :: thesis: E is Element of COM (S,M)
reconsider E0 = {} as Element of S by MEASURE1:7;
M . E0 = 0 by VALUED_0:def 19;
then A1: E0 is thin of M by MEASURE3:def 2;
E = E \/ E0 ;
hence E is Element of COM (S,M) by A1, MEASURE3:def 3; :: thesis: verum