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

proof

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))

proof

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₁( 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₁(n) from FUNCT_2:sch 4();
reconsider Bseq = Bseq as SetSequence of X ;
for n being Nat holds Bseq . n in F

proof

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;

then reconsider Bseq = Bseq as Set_Sequence of F by Def2;
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;

now :: thesis: for x being object st x in A /\ E9 holds
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;

then A /\ E9 c= union (rng Bseq) ;
then reconsider Bseq = Bseq as Covering of A /\ E9,F by Def3;
deffunc H₂( 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₂(n) from FUNCT_2:sch 4();
reconsider Cseq = Cseq as SetSequence of X ;
for n being Nat holds Cseq . n in F

proof

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;

then reconsider Cseq = Cseq as Set_Sequence of F by Def2;

now :: thesis: for x being object st x in A /\ (X \ E9) holds
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;

then A /\ (X \ E9) c= union (rng Cseq) ;
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

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;

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

for r being ExtReal st r in Svc (M,A) holds
((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r

proof

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;

then ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) is LowerBound of Svc (M,A) by XXREAL_2:def 2;
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;

hence E in sigma_Field (C_Meas M) by Th19; :: thesis: verum