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

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