let X be set ; :: thesis: for F being Field_Subset of X

for M being Measure of F holds F c= sigma_Field (C_Meas M)

let F be Field_Subset of X; :: thesis: for M being Measure of F holds F c= sigma_Field (C_Meas M)

let M be Measure of F; :: thesis: F c= sigma_Field (C_Meas M)

set C = C_Meas M;

let E be object ; :: according to TARSKI:def 3 :: thesis: ( not E in F or E in sigma_Field (C_Meas M) )

assume A1: E in F ; :: thesis: E in sigma_Field (C_Meas M)

then reconsider E9 = E as Subset of X ;

for A being Subset of X holds ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= (C_Meas M) . A

for M being Measure of F holds F c= sigma_Field (C_Meas M)

let F be Field_Subset of X; :: thesis: for M being Measure of F holds F c= sigma_Field (C_Meas M)

let M be Measure of F; :: thesis: F c= sigma_Field (C_Meas M)

set C = C_Meas M;

let E be object ; :: according to TARSKI:def 3 :: thesis: ( not E in F or E in sigma_Field (C_Meas M) )

assume A1: E in F ; :: thesis: E in sigma_Field (C_Meas M)

then reconsider E9 = E as Subset of X ;

for A being Subset of X holds ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= (C_Meas M) . A

proof

hence
E in sigma_Field (C_Meas M)
by Th19; :: thesis: verum
let A be Subset of X; :: thesis: ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= (C_Meas M) . A

set CA = ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9)));

A2: for seq being Covering of A,F holds ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= SUM (vol (M,seq))

((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r

then ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= inf (Svc (M,A)) by XXREAL_2:def 4;

hence ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= (C_Meas M) . A by Def8; :: thesis: verum

end;set CA = ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9)));

A2: for seq being Covering of A,F holds ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= SUM (vol (M,seq))

proof

for r being ExtReal st r in Svc (M,A) holds
let seq be Covering of A,F; :: thesis: ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= SUM (vol (M,seq))

deffunc H_{1}( Element of NAT ) -> Element of bool X = (seq . $1) /\ E9;

consider Bseq being sequence of (bool X) such that

A3: for n being Element of NAT holds Bseq . n = H_{1}(n)
from FUNCT_2:sch 4();

reconsider Bseq = Bseq as SetSequence of X ;

for n being Nat holds Bseq . n in F

A4: for x being set st x in A holds

ex n being Element of NAT st x in seq . n

then reconsider Bseq = Bseq as Covering of A /\ E9,F by Def3;

deffunc H_{2}( Element of NAT ) -> Element of bool X = (seq . $1) /\ (X \ E9);

consider Cseq being sequence of (bool X) such that

A11: for n being Element of NAT holds Cseq . n = H_{2}(n)
from FUNCT_2:sch 4();

reconsider Cseq = Cseq as SetSequence of X ;

for n being Nat holds Cseq . n in F

then reconsider Cseq = Cseq as Covering of A /\ (X \ E9),F by Def3;

A16: for n being Nat holds (vol (M,seq)) . n = ((vol (M,Bseq)) . n) + ((vol (M,Cseq)) . n)

then A21: (C_Meas M) . (A /\ (X \ E9)) <= SUM (vol (M,Cseq)) by XXREAL_2:3;

( (C_Meas M) . (A /\ E9) = inf (Svc (M,(A /\ E9))) & SUM (vol (M,Bseq)) in Svc (M,(A /\ E9)) ) by Def7, Def8;

then A22: (C_Meas M) . (A /\ E9) <= SUM (vol (M,Bseq)) by XXREAL_2:3;

( vol (M,Bseq) is nonnegative & vol (M,Cseq) is nonnegative ) by Th4;

then SUM (vol (M,seq)) = (SUM (vol (M,Bseq))) + (SUM (vol (M,Cseq))) by A16, Th3;

hence ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= SUM (vol (M,seq)) by A22, A21, XXREAL_3:36; :: thesis: verum

end;deffunc H

consider Bseq being sequence of (bool X) such that

A3: for n being Element of NAT holds Bseq . n = H

reconsider Bseq = Bseq as SetSequence of X ;

for n being Nat holds Bseq . n in F

proof

then reconsider Bseq = Bseq as Set_Sequence of F by Def2;
let n be Nat; :: thesis: Bseq . n in F

n in NAT by ORDINAL1:def 12;

then Bseq . n = (seq . n) /\ E9 by A3;

hence Bseq . n in F by A1, FINSUB_1:def 2; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

then Bseq . n = (seq . n) /\ E9 by A3;

hence Bseq . n in F by A1, FINSUB_1:def 2; :: thesis: verum

A4: for x being set st x in A holds

ex n being Element of NAT st x in seq . n

proof

let x be set ; :: thesis: ( x in A implies ex n being Element of NAT st x in seq . n )

assume A5: x in A ; :: thesis: ex n being Element of NAT st x in seq . n

A c= union (rng seq) by Def3;

then consider B being set such that

A6: x in B and

A7: B in rng seq by A5, TARSKI:def 4;

ex n being Element of NAT st B = seq . n by A7, FUNCT_2:113;

hence ex n being Element of NAT st x in seq . n by A6; :: thesis: verum

end;assume A5: x in A ; :: thesis: ex n being Element of NAT st x in seq . n

A c= union (rng seq) by Def3;

then consider B being set such that

A6: x in B and

A7: B in rng seq by A5, TARSKI:def 4;

ex n being Element of NAT st B = seq . n by A7, FUNCT_2:113;

hence ex n being Element of NAT st x in seq . n by A6; :: thesis: verum

now :: thesis: for x being object st x in A /\ E9 holds

x in union (rng Bseq)

then
A /\ E9 c= union (rng Bseq)
;x in union (rng Bseq)

let x be object ; :: thesis: ( x in A /\ E9 implies x in union (rng Bseq) )

assume A8: x in A /\ E9 ; :: thesis: x in union (rng Bseq)

then x in A by XBOOLE_0:def 4;

then consider n being Element of NAT such that

A9: x in seq . n by A4;

x in E9 by A8, XBOOLE_0:def 4;

then x in (seq . n) /\ E9 by A9, XBOOLE_0:def 4;

then A10: x in Bseq . n by A3;

Bseq . n in rng Bseq by FUNCT_2:4;

hence x in union (rng Bseq) by A10, TARSKI:def 4; :: thesis: verum

end;assume A8: x in A /\ E9 ; :: thesis: x in union (rng Bseq)

then x in A by XBOOLE_0:def 4;

then consider n being Element of NAT such that

A9: x in seq . n by A4;

x in E9 by A8, XBOOLE_0:def 4;

then x in (seq . n) /\ E9 by A9, XBOOLE_0:def 4;

then A10: x in Bseq . n by A3;

Bseq . n in rng Bseq by FUNCT_2:4;

hence x in union (rng Bseq) by A10, TARSKI:def 4; :: thesis: verum

then reconsider Bseq = Bseq as Covering of A /\ E9,F by Def3;

deffunc H

consider Cseq being sequence of (bool X) such that

A11: for n being Element of NAT holds Cseq . n = H

reconsider Cseq = Cseq as SetSequence of X ;

for n being Nat holds Cseq . n in F

proof

then reconsider Cseq = Cseq as Set_Sequence of F by Def2;
let n be Nat; :: thesis: Cseq . n in F

X in F by PROB_1:5;

then A12: X \ E9 in F by A1, PROB_1:6;

n in NAT by ORDINAL1:def 12;

then Cseq . n = (seq . n) /\ (X \ E9) by A11;

hence Cseq . n in F by A12, FINSUB_1:def 2; :: thesis: verum

end;X in F by PROB_1:5;

then A12: X \ E9 in F by A1, PROB_1:6;

n in NAT by ORDINAL1:def 12;

then Cseq . n = (seq . n) /\ (X \ E9) by A11;

hence Cseq . n in F by A12, FINSUB_1:def 2; :: thesis: verum

now :: thesis: for x being object st x in A /\ (X \ E9) holds

x in union (rng Cseq)

then
A /\ (X \ E9) c= union (rng Cseq)
;x in union (rng Cseq)

let x be object ; :: thesis: ( x in A /\ (X \ E9) implies x in union (rng Cseq) )

assume A13: x in A /\ (X \ E9) ; :: thesis: x in union (rng Cseq)

then x in A by XBOOLE_0:def 4;

then consider n being Element of NAT such that

A14: x in seq . n by A4;

x in X \ E9 by A13, XBOOLE_0:def 4;

then x in (seq . n) /\ (X \ E9) by A14, XBOOLE_0:def 4;

then A15: x in Cseq . n by A11;

Cseq . n in rng Cseq by FUNCT_2:4;

hence x in union (rng Cseq) by A15, TARSKI:def 4; :: thesis: verum

end;assume A13: x in A /\ (X \ E9) ; :: thesis: x in union (rng Cseq)

then x in A by XBOOLE_0:def 4;

then consider n being Element of NAT such that

A14: x in seq . n by A4;

x in X \ E9 by A13, XBOOLE_0:def 4;

then x in (seq . n) /\ (X \ E9) by A14, XBOOLE_0:def 4;

then A15: x in Cseq . n by A11;

Cseq . n in rng Cseq by FUNCT_2:4;

hence x in union (rng Cseq) by A15, TARSKI:def 4; :: thesis: verum

then reconsider Cseq = Cseq as Covering of A /\ (X \ E9),F by Def3;

A16: for n being Nat holds (vol (M,seq)) . n = ((vol (M,Bseq)) . n) + ((vol (M,Cseq)) . n)

proof

( (C_Meas M) . (A /\ (X \ E9)) = inf (Svc (M,(A /\ (X \ E9)))) & SUM (vol (M,Cseq)) in Svc (M,(A /\ (X \ E9))) )
by Def7, Def8;
let n be Nat; :: thesis: (vol (M,seq)) . n = ((vol (M,Bseq)) . n) + ((vol (M,Cseq)) . n)

A17: ( M . (seq . n) = (vol (M,seq)) . n & M . (Bseq . n) = (vol (M,Bseq)) . n ) by Def5;

A18: M . (Cseq . n) = (vol (M,Cseq)) . n by Def5;

n is Element of NAT by ORDINAL1:def 12;

then A19: ( Bseq . n = (seq . n) /\ E9 & Cseq . n = (seq . n) /\ (X \ E9) ) by A3, A11;

then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ (E9 \/ (X \ E9)) by XBOOLE_1:23;

then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ (E9 \/ X) by XBOOLE_1:39;

then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ X by XBOOLE_1:12;

then A20: (Bseq . n) \/ (Cseq . n) = seq . n by XBOOLE_1:28;

Bseq . n misses Cseq . n by A19, XBOOLE_1:76, XBOOLE_1:79;

hence (vol (M,seq)) . n = ((vol (M,Bseq)) . n) + ((vol (M,Cseq)) . n) by A20, A17, A18, MEASURE1:def 3; :: thesis: verum

end;A17: ( M . (seq . n) = (vol (M,seq)) . n & M . (Bseq . n) = (vol (M,Bseq)) . n ) by Def5;

A18: M . (Cseq . n) = (vol (M,Cseq)) . n by Def5;

n is Element of NAT by ORDINAL1:def 12;

then A19: ( Bseq . n = (seq . n) /\ E9 & Cseq . n = (seq . n) /\ (X \ E9) ) by A3, A11;

then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ (E9 \/ (X \ E9)) by XBOOLE_1:23;

then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ (E9 \/ X) by XBOOLE_1:39;

then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ X by XBOOLE_1:12;

then A20: (Bseq . n) \/ (Cseq . n) = seq . n by XBOOLE_1:28;

Bseq . n misses Cseq . n by A19, XBOOLE_1:76, XBOOLE_1:79;

hence (vol (M,seq)) . n = ((vol (M,Bseq)) . n) + ((vol (M,Cseq)) . n) by A20, A17, A18, MEASURE1:def 3; :: thesis: verum

then A21: (C_Meas M) . (A /\ (X \ E9)) <= SUM (vol (M,Cseq)) by XXREAL_2:3;

( (C_Meas M) . (A /\ E9) = inf (Svc (M,(A /\ E9))) & SUM (vol (M,Bseq)) in Svc (M,(A /\ E9)) ) by Def7, Def8;

then A22: (C_Meas M) . (A /\ E9) <= SUM (vol (M,Bseq)) by XXREAL_2:3;

( vol (M,Bseq) is nonnegative & vol (M,Cseq) is nonnegative ) by Th4;

then SUM (vol (M,seq)) = (SUM (vol (M,Bseq))) + (SUM (vol (M,Cseq))) by A16, Th3;

hence ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= SUM (vol (M,seq)) by A22, A21, XXREAL_3:36; :: thesis: verum

((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r

proof

then
((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) is LowerBound of Svc (M,A)
by XXREAL_2:def 2;
let r be ExtReal; :: thesis: ( r in Svc (M,A) implies ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r )

assume r in Svc (M,A) ; :: thesis: ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r

then ex G being Covering of A,F st r = SUM (vol (M,G)) by Def7;

hence ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r by A2; :: thesis: verum

end;assume r in Svc (M,A) ; :: thesis: ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r

then ex G being Covering of A,F st r = SUM (vol (M,G)) by Def7;

hence ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r by A2; :: thesis: verum

then ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= inf (Svc (M,A)) by XXREAL_2:def 4;

hence ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= (C_Meas M) . A by Def8; :: thesis: verum