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;

now

let E be set ; :: thesis: ( E in F implies 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) /\ E;
consider Bseq being Function of NAT ,(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 13;
then Bseq . n = (seq . n) /\ E 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:190;
hence ex n being Element of NAT st x in seq . n by A6; :: thesis: verum

end;

now

let x be set ; :: 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) /\ E by A9, XBOOLE_0:def 4;
then A10: x in Bseq . n by A3;
Bseq . n in rng Bseq by FUNCT_2:6;
hence x in union (rng Bseq) by A10, TARSKI:def 4; :: thesis: verum

end;

then A /\ E9 c= union (rng Bseq) by TARSKI:def 3;
then reconsider Bseq = Bseq as Covering of A /\ E9,F by Def3;
deffunc H₂( Element of NAT ) -> Element of bool X = (seq . $1) /\ (X \ E);
consider Cseq being Function of NAT ,(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:11;
then A12: X \ E in F by A1, PROB_1:12;
n in NAT by ORDINAL1:def 13;
then Cseq . n = (seq . n) /\ (X \ E) 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

let x be set ; :: 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 \ E) by A14, XBOOLE_0:def 4;
then A15: x in Cseq . n by A11;
Cseq . n in rng Cseq by FUNCT_2:6;
hence x in union (rng Cseq) by A15, TARSKI:def 4; :: thesis: verum

end;

then A /\ (X \ E9) c= union (rng Cseq) by TARSKI:def 3;
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 13;
then A19: ( Bseq . n = (seq . n) /\ E & Cseq . n = (seq . n) /\ (X \ E) ) by A3, A11;
then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ (E \/ (X \ E)) by XBOOLE_1:23;
then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ (E \/ 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 5; :: 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:38; :: thesis: verum

end;

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

proof

let r be ext-real number ; :: 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

end;

hence F c= sigma_Field (C_Meas M) by TARSKI:def 3; :: thesis: verum