let X be set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for D being non empty Subset-Family of X st ( for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) ) holds

D is SigmaField of X

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for D being non empty Subset-Family of X st ( for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) ) holds

D is SigmaField of X

let M be sigma_Measure of S; :: thesis: for D being non empty Subset-Family of X st ( for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) ) holds

D is SigmaField of X

let D be non empty Subset-Family of X; :: thesis: ( ( for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) ) implies D is SigmaField of X )

assume A1: for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) ; :: thesis: D is SigmaField of X

A2: for K being N_Sub_set_fam of X st K c= D holds

union K in D

X \ A in D

D9 is SigmaField of X ;

hence D is SigmaField of X ; :: thesis: verum

for M being sigma_Measure of S

for D being non empty Subset-Family of X st ( for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) ) holds

D is SigmaField of X

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for D being non empty Subset-Family of X st ( for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) ) holds

D is SigmaField of X

let M be sigma_Measure of S; :: thesis: for D being non empty Subset-Family of X st ( for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) ) holds

D is SigmaField of X

let D be non empty Subset-Family of X; :: thesis: ( ( for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) ) implies D is SigmaField of X )

assume A1: for A being set holds

( A in D iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) ; :: thesis: D is SigmaField of X

A2: for K being N_Sub_set_fam of X st K c= D holds

union K in D

proof

for A being set st A in D holds
let K be N_Sub_set_fam of X; :: thesis: ( K c= D implies union K in D )

consider F being sequence of (bool X) such that

A3: K = rng F by SUPINF_2:def 8;

assume A4: K c= D ; :: thesis: union K in D

A5: for n being Element of NAT holds F . n in D

( B in S & ex C being thin of M st F . n = B \/ C ) by A5, A1;

for n being Element of NAT holds F . n in COM (S,M)

F . n in COM (S,M) ;

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

then reconsider F = F as sequence of (COM (S,M)) by A7, FUNCT_2:3;

consider G being sequence of S such that

A9: for n being Element of NAT holds G . n in MeasPart (F . n) by Th15;

consider H being sequence of (bool X) such that

A10: for n being Element of NAT holds H . n = (F . n) \ (G . n) by Th16;

A11: for n being Element of NAT holds

( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M )

A12: for n being Element of NAT holds

( H . n c= L . n & M . (L . n) = 0. ) by Th17;

ex B being set st

( B in S & ex C being thin of M st union K = B \/ C )

end;consider F being sequence of (bool X) such that

A3: K = rng F by SUPINF_2:def 8;

assume A4: K c= D ; :: thesis: union K in D

A5: for n being Element of NAT holds F . n in D

proof

A6:
for n being Element of NAT ex B being set st
let n be Element of NAT ; :: thesis: F . n in D

F . n in K by A3, FUNCT_2:4;

hence F . n in D by A4; :: thesis: verum

end;F . n in K by A3, FUNCT_2:4;

hence F . n in D by A4; :: thesis: verum

( B in S & ex C being thin of M st F . n = B \/ C ) by A5, A1;

for n being Element of NAT holds F . n in COM (S,M)

proof

then A7:
for n being object st n in NAT holds
let n be Element of NAT ; :: thesis: F . n in COM (S,M)

ex B being set st

( B in S & ex C being thin of M st F . n = B \/ C ) by A6;

hence F . n in COM (S,M) by Def3; :: thesis: verum

end;ex B being set st

( B in S & ex C being thin of M st F . n = B \/ C ) by A6;

hence F . n in COM (S,M) by Def3; :: thesis: verum

F . n in COM (S,M) ;

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

then reconsider F = F as sequence of (COM (S,M)) by A7, FUNCT_2:3;

consider G being sequence of S such that

A9: for n being Element of NAT holds G . n in MeasPart (F . n) by Th15;

consider H being sequence of (bool X) such that

A10: for n being Element of NAT holds H . n = (F . n) \ (G . n) by Th16;

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

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

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

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

end;(F . n) \ (G . n) is thin of M by A11;

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

A12: for n being Element of NAT holds

( H . n c= L . n & M . (L . n) = 0. ) by Th17;

ex B being set st

( B in S & ex C being thin of M st union K = B \/ C )

proof

hence
union K in D
by A1; :: thesis: verum
set B = union (rng G);

take union (rng G) ; :: thesis: ( union (rng G) in S & ex C being thin of M st union K = (union (rng G)) \/ C )

A13: union (rng G) c= union (rng F)

end;take union (rng G) ; :: thesis: ( union (rng G) in S & ex C being thin of M st union K = (union (rng G)) \/ C )

A13: union (rng G) c= union (rng F)

proof

ex C being thin of M st union K = (union (rng G)) \/ C
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng G) or x in union (rng F) )

assume x in union (rng G) ; :: thesis: x in union (rng F)

then consider Z being set such that

A14: x in Z and

A15: Z in rng G by TARSKI:def 4;

dom G = NAT by FUNCT_2:def 1;

then consider n being object such that

A16: n in NAT and

A17: Z = G . n by A15, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A16;

set P = F . n;

A18: G . n c= F . n by A11;

ex P being set st

( P in rng F & x in P )

end;assume x in union (rng G) ; :: thesis: x in union (rng F)

then consider Z being set such that

A14: x in Z and

A15: Z in rng G by TARSKI:def 4;

dom G = NAT by FUNCT_2:def 1;

then consider n being object such that

A16: n in NAT and

A17: Z = G . n by A15, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A16;

set P = F . n;

A18: G . n c= F . n by A11;

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 A8, A14, A17, A18, FUNCT_1:def 3; :: thesis: verum

end;thus ( F . n in rng F & x in F . n ) by A8, A14, A17, A18, FUNCT_1:def 3; :: thesis: verum

proof

hence
( union (rng G) in S & ex C being thin of M st union K = (union (rng G)) \/ C )
; :: thesis: verum
for A being set st A in rng L holds

A is measure_zero of M

then A21: M . (union (rng L)) = 0. by MEASURE1:def 7;

set C = (union K) \ (union (rng G));

A22: union K = ((union K) \ (union (rng G))) \/ ((union (rng F)) /\ (union (rng G))) by A3, XBOOLE_1:51

.= (union (rng G)) \/ ((union K) \ (union (rng G))) by A13, XBOOLE_1:28 ;

reconsider C = (union K) \ (union (rng G)) as Subset of X ;

A23: C c= union (rng H)

then C is thin of M by A21, Def2;

then consider C being thin of M such that

A37: union K = (union (rng G)) \/ C by A22;

take C ; :: thesis: union K = (union (rng G)) \/ C

thus union K = (union (rng G)) \/ C by A37; :: 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 A19: A in rng L ; :: thesis: A is measure_zero of M

dom L = NAT by FUNCT_2:def 1;

then A20: ex n being object st

( n in NAT & A = L . n ) by A19, FUNCT_1:def 3;

rng L c= S by MEASURE2:def 1;

then reconsider A = A as Element of S by A19;

M . A = 0. by A12, A20;

hence A is measure_zero of M by MEASURE1:def 7; :: thesis: verum

end;assume A19: A in rng L ; :: thesis: A is measure_zero of M

dom L = NAT by FUNCT_2:def 1;

then A20: ex n being object st

( n in NAT & A = L . n ) by A19, FUNCT_1:def 3;

rng L c= S by MEASURE2:def 1;

then reconsider A = A as Element of S by A19;

M . A = 0. by A12, A20;

hence A is measure_zero of M by MEASURE1:def 7; :: thesis: verum

then A21: M . (union (rng L)) = 0. by MEASURE1:def 7;

set C = (union K) \ (union (rng G));

A22: union K = ((union K) \ (union (rng G))) \/ ((union (rng F)) /\ (union (rng G))) by A3, XBOOLE_1:51

.= (union (rng G)) \/ ((union K) \ (union (rng G))) by A13, XBOOLE_1:28 ;

reconsider C = (union K) \ (union (rng G)) as Subset of X ;

A23: 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 A24: x in C ; :: thesis: x in union (rng H)

then x in union (rng F) by A3, XBOOLE_0:def 5;

then consider Z being set such that

A25: x in Z and

A26: Z in rng F by TARSKI:def 4;

consider n being object such that

A27: n in NAT and

A28: Z = F . n by A8, A26, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A27;

A29: not x in union (rng G) by A24, XBOOLE_0:def 5;

not x in G . n

ex Z being set st

( x in Z & Z in rng H )

end;assume A24: x in C ; :: thesis: x in union (rng H)

then x in union (rng F) by A3, XBOOLE_0:def 5;

then consider Z being set such that

A25: x in Z and

A26: Z in rng F by TARSKI:def 4;

consider n being object such that

A27: n in NAT and

A28: Z = F . n by A8, A26, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A27;

A29: not x in union (rng G) by A24, XBOOLE_0:def 5;

not x in G . n

proof

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

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

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

hence contradiction by A29, A30, TARSKI:def 4; :: thesis: verum

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

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

hence contradiction by A29, A30, 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 A10, A31, 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 A10, A31, FUNCT_1:def 3; :: thesis: verum

proof

then
C c= union (rng L)
by A23;
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

A32: x in Z and

A33: Z in rng H by TARSKI:def 4;

dom H = NAT by FUNCT_2:def 1;

then consider n being object such that

A34: n in NAT and

A35: Z = H . n by A33, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A34;

n in dom L by A34, FUNCT_2:def 1;

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

H . n c= L . n by A12;

hence x in union (rng L) by A32, A35, A36, 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

A32: x in Z and

A33: Z in rng H by TARSKI:def 4;

dom H = NAT by FUNCT_2:def 1;

then consider n being object such that

A34: n in NAT and

A35: Z = H . n by A33, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A34;

n in dom L by A34, FUNCT_2:def 1;

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

H . n c= L . n by A12;

hence x in union (rng L) by A32, A35, A36, TARSKI:def 4; :: thesis: verum

then C is thin of M by A21, Def2;

then consider C being thin of M such that

A37: union K = (union (rng G)) \/ C by A22;

take C ; :: thesis: union K = (union (rng G)) \/ C

thus union K = (union (rng G)) \/ C by A37; :: thesis: verum

X \ A in D

proof

then reconsider D9 = D as non empty compl-closed sigma-additive Subset-Family of X by A2, MEASURE1:def 1, MEASURE1:def 5;
let A be set ; :: thesis: ( A in D implies X \ A in D )

assume A38: A in D ; :: thesis: X \ A in D

ex Q being set st

( Q in S & ex W being thin of M st X \ A = Q \/ W )

end;assume A38: A in D ; :: thesis: X \ A in D

ex Q being set st

( Q in S & ex W being thin of M st X \ A = Q \/ W )

proof

hence
X \ A in D
by A1; :: thesis: verum
consider B being set such that

A39: B in S and

A40: ex C being thin of M st A = B \/ C by A1, A38;

set P = X \ B;

consider C being thin of M such that

A41: A = B \/ C by A40;

consider G being set such that

A42: G in S and

A43: C c= G and

A44: M . G = 0. by Def2;

set Q = (X \ B) \ G;

A45: X \ A = (X \ B) \ C by A41, XBOOLE_1:41;

A46: ex W being thin of M st X \ A = ((X \ B) \ G) \/ W

X \ B in S by A39, MEASURE1:def 1;

hence ( (X \ B) \ G in S & ex W being thin of M st X \ A = ((X \ B) \ G) \/ W ) by A42, A46, MEASURE1:6; :: thesis: verum

end;A39: B in S and

A40: ex C being thin of M st A = B \/ C by A1, A38;

set P = X \ B;

consider C being thin of M such that

A41: A = B \/ C by A40;

consider G being set such that

A42: G in S and

A43: C c= G and

A44: M . G = 0. by Def2;

set Q = (X \ B) \ G;

A45: X \ A = (X \ B) \ C by A41, XBOOLE_1:41;

A46: ex W being thin of M st X \ A = ((X \ B) \ G) \/ W

proof

take
(X \ B) \ G
; :: thesis: ( (X \ B) \ G in S & ex W being thin of M st X \ A = ((X \ B) \ G) \/ W )
set W = (X \ B) /\ (G \ C);

(X \ B) /\ (G \ C) c= X \ B by XBOOLE_1:17;

then reconsider W = (X \ B) /\ (G \ C) as Subset of X by XBOOLE_1:1;

reconsider W = W as thin of M by A42, A44, Def2;

take W ; :: thesis: X \ A = ((X \ B) \ G) \/ W

thus X \ A = ((X \ B) \ G) \/ W by A43, A45, XBOOLE_1:117; :: thesis: verum

end;(X \ B) /\ (G \ C) c= X \ B by XBOOLE_1:17;

then reconsider W = (X \ B) /\ (G \ C) as Subset of X by XBOOLE_1:1;

reconsider W = W as thin of M by A42, A44, Def2;

take W ; :: thesis: X \ A = ((X \ B) \ G) \/ W

thus X \ A = ((X \ B) \ G) \/ W by A43, A45, XBOOLE_1:117; :: thesis: verum

X \ B in S by A39, MEASURE1:def 1;

hence ( (X \ B) \ G in S & ex W being thin of M st X \ A = ((X \ B) \ G) \/ W ) by A42, A46, MEASURE1:6; :: thesis: verum

D9 is SigmaField of X ;

hence D is SigmaField of X ; :: thesis: verum