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

proof

let K be N_Sub_set_fam of X; :: thesis: ( K c= D implies union K in D )
consider F being Function of NAT,(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

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;

A6: for n being Element of NAT ex B being set st
( B in S & ex C being thin of M st F . n = B \/ C )

proof

let n be Element of NAT ; :: thesis: ex B being set st
( B in S & ex C being thin of M st F . n = B \/ C )
F . n in D by A5;
hence ex B being set st
( B in S & ex C being thin of M st F . n = B \/ C ) by A1; :: thesis: verum

end;

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

proof

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

end;

then A7: for n being set st n in NAT holds
F . n in COM (S,M) ;
A8: dom F = NAT by FUNCT_2:def 1;
then reconsider F = F as Function of NAT,(COM (S,M)) by A7, FUNCT_2:3;
consider G being Function of NAT,S such that
A9: 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
A10: for n being Element of NAT holds H . n = (F . n) \ (G . n) by Th19;
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

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 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 A11;
hence H . n is thin of M by A10; :: thesis: verum

end;

then consider L being Function of NAT,S such that
A12: for n being Element of NAT holds
( H . n c= L . n & M . (L . n) = 0. ) by Th20;
ex B being set st
( B in S & ex C being thin of M st union K = B \/ C )

proof

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)

proof

let x be set ; :: 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 set 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

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;

hence x in union (rng F) by TARSKI:def 4; :: thesis: verum

end;

ex C being thin of M st union K = (union (rng G)) \/ 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 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 set 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;

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

let x be set ; :: 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 set 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

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 A31: x in (F . n) \ (G . n) by A25, A28, 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 A10, A31, FUNCT_1:def 3; :: 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
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 set 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;

then C c= union (rng L) by A23, XBOOLE_1:1;
then C is thin of M by A21, Def3;
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;

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

end;

hence union K in D by A1; :: thesis: verum

end;

for A being set st A in D holds
X \ A in D

proof

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 )

proof

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

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

take (X \ B) \ G ; :: thesis: ( (X \ B) \ G in S & 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;

hence X \ A in D by A1; :: thesis: verum

end;

then reconsider D9 = D as non empty compl-closed sigma-additive Subset-Family of X by A2, MEASURE1:def 1, MEASURE1:def 5;
D9 is SigmaField of X ;
hence D is SigmaField of X ; :: thesis: verum