set B = {} ;

defpred S_{1}[ 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. )

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 & S_{1}[x,y] )

A4: for x being object st x in COM (S,M) holds

S_{1}[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

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 ; :: 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

defpred S

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

{} is Subset of X
by XBOOLE_1:2;
take
{}
; :: thesis: ( {} in S & {} c= {} & M . {} = 0. )

thus ( {} in S & {} c= {} & M . {} = 0. ) by PROB_1:4, VALUED_0:def 19; :: thesis: verum

end;thus ( {} in S & {} c= {} & M . {} = 0. ) by PROB_1:4, VALUED_0:def 19; :: thesis: verum

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 & S

proof

consider comM being Function of (COM (S,M)),ExtREAL such that
let x be object ; :: thesis: ( x in COM (S,M) implies ex y being object st

( y in ExtREAL & S_{1}[x,y] ) )

assume x in COM (S,M) ; :: thesis: ex y being object st

( y in ExtREAL & S_{1}[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 & S_{1}[x,M . B] )

thus ( M . B in ExtREAL & S_{1}[x,M . B] )
by A3, Th19; :: thesis: verum

end;( y in ExtREAL & S

assume x in COM (S,M) ; :: thesis: ex y being object st

( y in ExtREAL & S

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 & S

thus ( M . B in ExtREAL & S

A4: for x being object st x in COM (S,M) holds

S

A5: for B being set st B in S holds

for C being thin of M holds comM . (B \/ C) = M . B

proof

A7:
for F being Sep_Sequence of (COM (S,M)) holds SUM (comM * F) = comM . (union (rng F))
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, Def3;

hence comM . (B \/ C) = M . B by A4, A6; :: thesis: verum

end;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, Def3;

hence comM . (B \/ C) = M . B by A4, A6; :: thesis: verum

proof

A48:
for x being Element of COM (S,M) holds 0. <= comM . x
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 )

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

A16: B = union (rng G) ;

A17: dom F = NAT by FUNCT_2:def 1;

A18: B c= union (rng F)

A44: for n being Element of NAT holds comM . (F . n) = M . (G . 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 A47, MEASURE1:def 6, XXREAL_0:1;

hence SUM (comM * F) = comM . (union (rng F)) by A5, A16, A24; :: thesis: verum

end;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

for n being Element of NAT holds H . n is thin of M
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;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

proof

then consider L being sequence of S such that
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;(F . n) \ (G . n) is thin of M by A10;

hence H . n is thin of M by A9; :: thesis: verum

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

consider B being set such that
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

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 A15, XBOOLE_1:3, XBOOLE_1:27;

hence G . n misses G . m ; :: thesis: verum

end;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

then A15:
( G . n c= F . n & G . m c= F . m )
;
let n be object ; :: thesis: G . n c= F . n

end;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 A15, XBOOLE_1:3, XBOOLE_1:27;

hence G . n misses G . m ; :: thesis: verum

A16: B = union (rng G) ;

A17: dom F = NAT by FUNCT_2:def 1;

A18: B c= union (rng F)

proof

A24:
ex C being thin of M st union (rng F) = B \/ C
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 A16, TARSKI:def 4;

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 A20, FUNCT_1:def 3;

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 )

end;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 object such that

A21: n in NAT and

A22: Z = G . n by A20, FUNCT_1:def 3;

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

hence
x in union (rng F)
by TARSKI:def 4; :: thesis: verum
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 3; :: thesis: verum

end;thus ( F . n in rng F & x in F . n ) by A17, A19, A22, A23, FUNCT_1:def 3; :: thesis: verum

proof

reconsider G = G as Sep_Sequence of S by A12, PROB_2:def 2;
for A being set st A in rng L holds

A is measure_zero of M

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 A18, XBOOLE_1:28 ;

reconsider C = (union (rng F)) \ B as Subset of X ;

A29: C c= union (rng H)

then C is thin of M by A27, Def2;

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;A is measure_zero of M

proof

then
union (rng L) is measure_zero of M
by MEASURE2:14;
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 A25, FUNCT_1:def 3;

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 7; :: thesis: verum

end;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 A25, FUNCT_1:def 3;

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 7; :: thesis: verum

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 A18, XBOOLE_1:28 ;

reconsider C = (union (rng F)) \ B as Subset of X ;

A29: C c= union (rng H)

proof

union (rng H) c= union (rng L)
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 A17, A32, FUNCT_1:def 3;

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

ex Z being set st

( x in Z & Z in rng H )

end;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 A17, A32, FUNCT_1:def 3;

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

then A37:
x in (F . n) \ (G . n)
by A31, A34, XBOOLE_0:def 5;
dom G = NAT
by FUNCT_2:def 1;

then A36: G . n in rng G by FUNCT_1:def 3;

assume x in G . n ; :: thesis: contradiction

hence contradiction by A35, A36, TARSKI:def 4; :: thesis: verum

end;then A36: G . n in rng G by FUNCT_1:def 3;

assume x in G . n ; :: thesis: contradiction

hence contradiction by A35, A36, TARSKI:def 4; :: thesis: verum

ex Z being set st

( x in Z & Z in rng H )

proof

hence
x in union (rng H)
by TARSKI:def 4; :: thesis: verum
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 3; :: thesis: verum

end;dom H = NAT by FUNCT_2:def 1;

hence ( x in H . n & H . n in rng H ) by A9, A37, FUNCT_1:def 3; :: thesis: verum

proof

then
C c= union (rng L)
by A29;
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 A39, FUNCT_1:def 3;

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 3;

H . n c= L . n by A11;

hence x in union (rng L) by A38, A41, A42, TARSKI:def 4; :: thesis: verum

end;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 A39, FUNCT_1:def 3;

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 3;

H . n c= L . n by A11;

hence x in union (rng L) by A38, A41, A42, TARSKI:def 4; :: thesis: verum

then C is thin of M by A27, Def2;

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

A44: for n being Element of NAT holds comM . (F . n) = M . (G . n)

proof

A46:
for n being Element of NAT holds (comM * F) . n = (M * G) . n
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;(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

proof

then
for n being Element of NAT holds (M * G) . n <= (comM * F) . n
;
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;(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

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 A47, MEASURE1:def 6, XXREAL_0:1;

hence SUM (comM * F) = comM . (union (rng F)) by A5, A16, A24; :: thesis: verum

proof

{} = {} \/ C
;
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 A4, A50;

hence 0. <= comM . x by MEASURE1:def 2; :: thesis: verum

end;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 A4, A50;

hence 0. <= comM . x by MEASURE1:def 2; :: thesis: verum

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 ; :: 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