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. )
proof
take {} ; :: thesis: ( {} in S & {} c= {} & M . {} = 0. )
thus ( {} in S & {} c= {} & M . {} = 0. ) by ; :: thesis: verum
end;
{} is Subset of X by XBOOLE_1:2;
then reconsider C = {} as thin of M by ;
A2: for x being object st x in COM (S,M) holds
ex y being object st
( y in ExtREAL & S1[x,y] )
proof
let x be object ; :: thesis: ( x in COM (S,M) implies ex y being object st
( y in ExtREAL & S1[x,y] ) )

assume x in COM (S,M) ; :: thesis: ex y being object st
( y in ExtREAL & S1[x,y] )

then consider B being set such that
A3: ( B in S & ex C being thin of M st x = B \/ C ) by Def3;
take M . B ; :: thesis: ( M . B in ExtREAL & S1[x,M . B] )
thus ( M . B in ExtREAL & S1[x,M . B] ) by ; :: thesis: verum
end;
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 A5: for B being set st B in S holds
for C being thin of M holds comM . (B \/ C) = M . B
proof
let B be set ; :: thesis: ( B in S implies for C being thin of M holds comM . (B \/ C) = M . B )
assume A6: B in S ; :: thesis: for C being thin of M holds comM . (B \/ C) = M . B
let C be thin of M; :: thesis: comM . (B \/ C) = M . B
B \/ C in COM (S,M) by ;
hence comM . (B \/ C) = M . B by A4, A6; :: thesis: verum
end;
A7: for F being Sep_Sequence of (COM (S,M)) holds SUM (comM * F) = comM . (union (rng F))
proof
let F be Sep_Sequence of (COM (S,M)); :: thesis: SUM (comM * F) = comM . (union (rng F))
consider G being sequence of S such that
A8: for n being Element of NAT holds G . n in MeasPart (F . n) by Th15;
consider H being sequence of (bool X) such that
A9: for n being Element of NAT holds H . n = (F . n) \ (G . n) by Th16;
A10: for n being Element of NAT holds
( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M )
proof
let n be Element of NAT ; :: thesis: ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M )
G . n in MeasPart (F . n) by A8;
hence ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M ) by Def4; :: thesis: verum
end;
for n being Element of NAT holds H . n is thin of M
proof
let n be Element of NAT ; :: thesis: H . n is thin of M
(F . n) \ (G . n) is thin of M by A10;
hence H . n is thin of M by A9; :: thesis: verum
end;
then consider L being sequence of S such that
A11: for n being Element of NAT holds
( H . n c= L . n & M . (L . n) = 0. ) by Th17;
A12: for n, m being object st n <> m holds
G . n misses G . m
proof
let n, m be object ; :: thesis: ( n <> m implies G . n misses G . m )
A13: dom F = NAT by FUNCT_2:def 1
.= dom G by FUNCT_2:def 1 ;
for n being object holds G . n c= F . n
proof
let n be object ; :: thesis: G . n c= F . n
per cases ( n in dom F or not n in dom F ) ;
suppose n in dom F ; :: thesis: G . n c= F . n
hence G . n c= F . n by A10; :: thesis: verum
end;
suppose A14: not n in dom F ; :: thesis: G . n c= F . n
then F . n = {} by FUNCT_1:def 2
.= G . n by ;
hence G . n c= F . n ; :: thesis: verum
end;
end;
end;
then A15: ( G . n c= F . n & G . m c= F . m ) ;
assume n <> m ; :: thesis: G . n misses G . m
then F . n misses F . m by PROB_2:def 2;
then (F . n) /\ (F . m) = {} ;
then (G . n) /\ (G . m) = {} by ;
hence G . n misses G . m ; :: thesis: verum
end;
consider B being set such that
A16: B = union (rng G) ;
A17: dom F = NAT by FUNCT_2:def 1;
A18: B c= union (rng F)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in union (rng F) )
assume x in B ; :: thesis: x in union (rng F)
then consider Z being set such that
A19: x in Z and
A20: Z in rng G by ;
dom G = NAT by FUNCT_2:def 1;
then consider n being object such that
A21: n in NAT and
A22: Z = G . n by ;
reconsider n = n as Element of NAT by A21;
set P = F . n;
A23: G . n c= F . n by A10;
ex P being set st
( P in rng F & x in P )
proof
take F . n ; :: thesis: ( F . n in rng F & x in F . n )
thus ( F . n in rng F & x in F . n ) by ; :: thesis: verum
end;
hence x in union (rng F) by TARSKI:def 4; :: thesis: verum
end;
A24: ex C being thin of M st union (rng F) = B \/ C
proof
for A being set st A in rng L holds
A is measure_zero of M
proof
let A be set ; :: thesis: ( A in rng L implies A is measure_zero of M )
assume A25: A in rng L ; :: thesis: A is measure_zero of M
dom L = NAT by FUNCT_2:def 1;
then A26: ex n being object st
( n in NAT & A = L . n ) by ;
rng L c= S by MEASURE2:def 1;
then reconsider A = A as Element of S by A25;
M . A = 0. by ;
hence A is measure_zero of M by MEASURE1:def 7; :: thesis: verum
end;
then union (rng L) is measure_zero of M by MEASURE2:14;
then A27: M . (union (rng L)) = 0. by MEASURE1:def 7;
set C = (union (rng F)) \ B;
A28: union (rng F) = ((union (rng F)) \ B) \/ ((union (rng F)) /\ B) by XBOOLE_1:51
.= B \/ ((union (rng F)) \ B) by ;
reconsider C = (union (rng F)) \ B as Subset of X ;
A29: C c= union (rng H)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in union (rng H) )
assume A30: x in C ; :: thesis: x in union (rng H)
then x in union (rng F) by XBOOLE_0:def 5;
then consider Z being set such that
A31: x in Z and
A32: Z in rng F by TARSKI:def 4;
consider n being object such that
A33: n in NAT and
A34: Z = F . n by ;
reconsider n = n as Element of NAT by A33;
A35: not x in union (rng G) by ;
not x in G . n then A37: x in (F . n) \ (G . n) by ;
ex Z being set st
( x in Z & Z in rng H )
proof
take H . n ; :: thesis: ( x in H . n & H . n in rng H )
dom H = NAT by FUNCT_2:def 1;
hence ( x in H . n & H . n in rng H ) by ; :: thesis: verum
end;
hence x in union (rng H) by TARSKI:def 4; :: thesis: verum
end;
union (rng H) c= union (rng L)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng H) or x in union (rng L) )
assume x in union (rng H) ; :: thesis: x in union (rng L)
then consider Z being set such that
A38: x in Z and
A39: Z in rng H by TARSKI:def 4;
dom H = NAT by FUNCT_2:def 1;
then consider n being object such that
A40: n in NAT and
A41: Z = H . n by ;
reconsider n = n as Element of NAT by A40;
n in dom L by ;
then A42: L . n in rng L by FUNCT_1:def 3;
H . n c= L . n by A11;
hence x in union (rng L) by ; :: thesis: verum
end;
then C c= union (rng L) by A29;
then C is thin of M by ;
then consider C being thin of M such that
A43: union (rng F) = B \/ C by A28;
take C ; :: thesis: union (rng F) = B \/ C
thus union (rng F) = B \/ C by A43; :: thesis: verum
end;
reconsider G = G as Sep_Sequence of S by ;
A44: for n being Element of NAT holds comM . (F . n) = M . (G . n)
proof
let n be Element of NAT ; :: thesis: comM . (F . n) = M . (G . n)
(F . n) \ (G . n) is thin of M by A10;
then consider C being thin of M such that
A45: C = (F . n) \ (G . n) ;
F . n = ((F . n) /\ (G . n)) \/ ((F . n) \ (G . n)) by XBOOLE_1:51
.= (G . n) \/ C by ;
hence comM . (F . n) = M . (G . n) by A5; :: thesis: verum
end;
A46: for n being Element of NAT holds (comM * F) . n = (M * G) . n
proof
let n be Element of NAT ; :: thesis: (comM * F) . n = (M * G) . n
(comM * F) . n = comM . (F . n) by FUNCT_2:15
.= M . (G . n) by A44
.= (M * G) . n by FUNCT_2:15 ;
hence (comM * F) . n = (M * G) . n ; :: thesis: verum
end;
then for n being Element of NAT holds (M * G) . n <= (comM * F) . n ;
then A47: SUM (M * G) <= SUM (comM * F) by SUPINF_2:43;
for n being Element of NAT holds (comM * F) . n <= (M * G) . n by A46;
then SUM (comM * F) <= SUM (M * G) by SUPINF_2:43;
then ( SUM (M * G) = M . (union (rng G)) & SUM (comM * F) = SUM (M * G) ) by ;
hence SUM (comM * F) = comM . (union (rng F)) by A5, A16, A24; :: thesis: verum
end;
A48: for x being Element of COM (S,M) holds 0. <= comM . x
proof
let x be Element of COM (S,M); :: thesis: 0. <= comM . x
consider B being set such that
A49: B in S and
A50: ex C being thin of M st x = B \/ C by Def3;
reconsider B = B as Element of S by A49;
comM . x = M . B by ;
hence 0. <= comM . x by MEASURE1:def 2; :: thesis: verum
end;
{} = {} \/ C ;
then comM . {} = M . {} by
.= 0. by VALUED_0:def 19 ;
then reconsider comM = comM as sigma_Measure of (COM (S,M)) by ;
take comM ; :: thesis: 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; :: thesis: verum