set B = {} ;
defpred S1[ object , object ] means for x, y being set st x in COM (S,M) & x = $1 & y = $2 holds
for B being set st B in S holds
for C being thin of M st x = B \/ C holds
y = M . B;
A1:
ex B1 being set st
( B1 in S & {} c= B1 & M . B1 = 0. )
{} is Subset of X
by XBOOLE_1:2;
then reconsider C = {} as thin of M by A1, Def2;
A2:
for x being object st x in COM (S,M) holds
ex y being object st
( y in ExtREAL & S1[x,y] )
consider comM being Function of (COM (S,M)),ExtREAL such that
A4:
for x being object st x in COM (S,M) holds
S1[x,comM . x]
from FUNCT_2:sch 1(A2);
A5:
for B being set st B in S holds
for C being thin of M holds comM . (B \/ C) = M . B
A7:
for F being Sep_Sequence of (COM (S,M)) holds SUM (comM * F) = comM . (union (rng F))
A48:
for x being Element of COM (S,M) holds 0. <= comM . x
{} = {} \/ C
;
then comM . {} =
M . {}
by A5, PROB_1:4
.=
0.
by VALUED_0:def 19
;
then reconsider comM = comM as sigma_Measure of (COM (S,M)) by A48, A7, MEASURE1:def 2, MEASURE1:def 6, VALUED_0:def 19;
take
comM
; for B being set st B in S holds
for C being thin of M holds comM . (B \/ C) = M . B
thus
for B being set st B in S holds
for C being thin of M holds comM . (B \/ C) = M . B
by A5; verum