set B = {} ;
defpred S₁[ set , set ] 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 PROB_1:10, VALUED_0:def 19; :: thesis: verum

end;

{} is Subset of X by XBOOLE_1:2;
then reconsider C = {} as thin of M by A1, Def3;
A2: for x being set st x in COM S,M holds
ex y being set st
( y in ExtREAL & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in COM S,M implies ex y being set st
( y in ExtREAL & S₁[x,y] ) )
assume x in COM S,M ; :: thesis: ex y being set st
( y in ExtREAL & S₁[x,y] )
then consider B being set such that
A3: ( B in S & ex C being thin of M st x = B \/ C ) by Def4;
take M . B ; :: thesis: ( M . B in ExtREAL & S₁[x,M . B] )
thus ( M . B in ExtREAL & S₁[x,M . B] ) by A3, Th22; :: thesis: verum

end;

consider comM being Function of (COM S,M),ExtREAL such that
A4: for x being set st x in COM S,M holds
S₁[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

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 A6, Def4;
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 Function of NAT ,S such that
A8: for n being Element of NAT holds G . n in MeasPart (F . n) by Th18;
consider H being Function of NAT ,(bool X) such that
A9: for n being Element of NAT holds H . n = (F . n) \ (G . n) by Th19;
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 Def5; :: 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 Function of NAT ,S such that
A11: for n being Element of NAT holds
( H . n c= L . n & M . (L . n) = 0. ) by Th20;
A12: for n, m being set st n <> m holds
G . n misses G . m

proof

let n, m be set ; :: 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 set holds G . n c= F . n

proof

let n be set ; :: 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 4
.= G . n by A13, A14, FUNCT_1:def 4 ;
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 3;
then (F . n) /\ (F . m) = {} by XBOOLE_0:def 7;
then (G . n) /\ (G . m) = {} by A15, XBOOLE_1:3, XBOOLE_1:27;
hence G . n misses G . m by XBOOLE_0:def 7; :: 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 set ; :: 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 A16, TARSKI:def 4;
dom G = NAT by FUNCT_2:def 1;
then consider n being set such that
A21: n in NAT and
A22: Z = G . n by A20, FUNCT_1:def 5;
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 A17, A19, A22, A23, FUNCT_1:def 5; :: 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 set st
( n in NAT & A = L . n ) by A25, FUNCT_1:def 5;
rng L c= S by MEASURE2:def 1;
then reconsider A = A as Element of S by A25;
M . A = 0. by A11, A26;
hence A is measure_zero of M by MEASURE1:def 13; :: thesis: verum

end;

then union (rng L) is measure_zero of M by MEASURE2:16;
then A27: M . (union (rng L)) = 0. by MEASURE1:def 13;
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 A18, XBOOLE_1:28 ;
reconsider C = (union (rng F)) \ B as Subset of X ;
A29: C c= union (rng H)

proof

let x be set ; :: 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 set such that
A33: n in NAT and
A34: Z = F . n by A17, A32, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A33;
A35: not x in union (rng G) by A16, A30, XBOOLE_0:def 5;
not x in G . n

proof

dom G = NAT by FUNCT_2:def 1;
then A36: G . n in rng G by FUNCT_1:def 5;
assume x in G . n ; :: thesis: contradiction
hence contradiction by A35, A36, TARSKI:def 4; :: thesis: verum

end;

then A37: x in (F . n) \ (G . n) by A31, A34, XBOOLE_0:def 5;
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 A9, A37, FUNCT_1:def 5; :: 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 set ; :: 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 set such that
A40: n in NAT and
A41: Z = H . n by A39, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A40;
n in dom L by A40, FUNCT_2:def 1;
then A42: L . n in rng L by FUNCT_1:def 5;
H . n c= L . n by A11;
hence x in union (rng L) by A38, A41, A42, TARSKI:def 4; :: thesis: verum

end;

then C c= union (rng L) by A29, XBOOLE_1:1;
then C is thin of M by A27, Def3;
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 A12, PROB_2:def 3;
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 A10, A45, XBOOLE_1:28 ;
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:21
.= M . (G . n) by A44
.= (M * G) . n by FUNCT_2:21 ;
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:62;
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:62;
then ( SUM (M * G) = M . (union (rng G)) & SUM (comM * F) = SUM (M * G) ) by A47, MEASURE1:def 11, XXREAL_0:1;
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 Def4;
reconsider B = B as Element of S by A49;
comM . x = M . B by A4, A50;
hence 0. <= comM . x by MEASURE1:def 4; :: thesis: verum

end;

{} = {} \/ C ;
then comM . {} = M . {} by A5, PROB_1:10
.= 0. by VALUED_0:def 19 ;
then reconsider comM = comM as sigma_Measure of (COM S,M) by A48, A7, MEASURE1:def 4, MEASURE1:def 11, VALUED_0:def 19;
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