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 E' = E as Subset of X ;
for A being Subset of X holds ((C_Meas M) . (A /\ E')) + ((C_Meas M) . (A /\ (X \ E'))) <= (C_Meas M) . A

proof

let A be Subset of X; :: thesis: ((C_Meas M) . (A /\ E')) + ((C_Meas M) . (A /\ (X \ E'))) <= (C_Meas M) . A
AA: for seq being Covering of A,F holds ((C_Meas M) . (A /\ E')) + ((C_Meas M) . (A /\ (X \ E'))) <= SUM (vol M,seq)

proof

let seq be Covering of A,F; :: thesis: ((C_Meas M) . (A /\ E')) + ((C_Meas M) . (A /\ (X \ E'))) <= 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 DDef4;
A5: 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 A51: x in A ; :: thesis: ex n being Element of NAT st x in seq . n
A c= union (rng seq) by Def2;
then consider B being set such that
A52: ( x in B & B in rng seq ) by A51, TARSKI:def 4;
ex n being Element of NAT st B = seq . n by A52, FUNCT_2:190;
hence ex n being Element of NAT st x in seq . n by A52; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in A /\ E' implies x in union (rng Bseq) )
assume x in A /\ E' ; :: thesis: x in union (rng Bseq)
then A6: ( x in A & x in E' ) by XBOOLE_0:def 4;
then consider n being Element of NAT such that
A7: x in seq . n by A5;
x in (seq . n) /\ E by A6, A7, XBOOLE_0:def 4;
then A8: x in Bseq . n by A3;
Bseq . n in rng Bseq by FUNCT_2:6;
hence x in union (rng Bseq) by A8, TARSKI:def 4; :: thesis: verum

end;

then A /\ E' c= union (rng Bseq) by TARSKI:def 3;
then reconsider Bseq = Bseq as Covering of A /\ E',F by Def2;
deffunc H₂( Element of NAT ) -> Element of bool X = (seq . $1) /\ (X \ E);
consider Cseq being Function of NAT ,(bool X) such that
B1: 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
n in NAT by ORDINAL1:def 13;
then B2: Cseq . n = (seq . n) /\ (X \ E) by B1;
X in F by PROB_1:11;
then ( X \ E in F & seq . n in F ) by A1, PROB_1:12;
hence Cseq . n in F by B2, FINSUB_1:def 2; :: thesis: verum

end;

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

now

let x be set ; :: thesis: ( x in A /\ (X \ E') implies x in union (rng Cseq) )
assume x in A /\ (X \ E') ; :: thesis: x in union (rng Cseq)
then B3: ( x in A & x in X \ E' ) by XBOOLE_0:def 4;
then consider n being Element of NAT such that
B4: x in seq . n by A5;
x in (seq . n) /\ (X \ E) by B3, B4, XBOOLE_0:def 4;
then B5: x in Cseq . n by B1;
Cseq . n in rng Cseq by FUNCT_2:6;
hence x in union (rng Cseq) by B5, TARSKI:def 4; :: thesis: verum

end;

then A /\ (X \ E') c= union (rng Cseq) by TARSKI:def 3;
then reconsider Cseq = Cseq as Covering of A /\ (X \ E'),F by Def2;
C1: 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)
n is Element of NAT by ORDINAL1:def 13;
then C2: ( Bseq . n = (seq . n) /\ E & Cseq . n = (seq . n) /\ (X \ E) ) by A3, B1;
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 C3: (Bseq . n) \/ (Cseq . n) = seq . n by XBOOLE_1:28;
C4: Bseq . n misses Cseq . n by C2, XBOOLE_1:76, XBOOLE_1:79;
( M . (seq . n) = (vol M,seq) . n & M . (Bseq . n) = (vol M,Bseq) . n & M . (Cseq . n) = (vol M,Cseq) . n ) by Def4;
hence (vol M,seq) . n = ((vol M,Bseq) . n) + ((vol M,Cseq) . n) by C4, C3, MEASURE1:def 5; :: thesis: verum

end;

( vol M,Bseq is nonnegative & vol M,Cseq is nonnegative ) by Th13;
then C5: SUM (vol M,seq) = (SUM (vol M,Bseq)) + (SUM (vol M,Cseq)) by C1, MEASURE74;
C6: (C_Meas M) . (A /\ E') = inf (Svc M,(A /\ E')) by Def10;
SUM (vol M,Bseq) in Svc M,(A /\ E') by Def8;
then C7: (C_Meas M) . (A /\ E') <= SUM (vol M,Bseq) by C6, XXREAL_2:3;
C8: (C_Meas M) . (A /\ (X \ E')) = inf (Svc M,(A /\ (X \ E'))) by Def10;
SUM (vol M,Cseq) in Svc M,(A /\ (X \ E')) by Def8;
then (C_Meas M) . (A /\ (X \ E')) <= SUM (vol M,Cseq) by C8, XXREAL_2:3;
hence ((C_Meas M) . (A /\ E')) + ((C_Meas M) . (A /\ (X \ E'))) <= SUM (vol M,seq) by C5, C7, XXREAL_3:38; :: thesis: verum

end;

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

proof

let r be ext-real number ; :: thesis: ( r in Svc M,A implies ((C_Meas M) . (A /\ E')) + ((C_Meas M) . (A /\ (X \ E'))) <= r )
assume r in Svc M,A ; :: thesis: ((C_Meas M) . (A /\ E')) + ((C_Meas M) . (A /\ (X \ E'))) <= r
then ex G being Covering of A,F st r = SUM (vol M,G) by Def8;
hence ((C_Meas M) . (A /\ E')) + ((C_Meas M) . (A /\ (X \ E'))) <= r by AA; :: thesis: verum

end;

then ((C_Meas M) . (A /\ E')) + ((C_Meas M) . (A /\ (X \ E'))) is LowerBound of Svc M,A by XXREAL_2:def 2;
then ((C_Meas M) . (A /\ E')) + ((C_Meas M) . (A /\ (X \ E'))) <= inf (Svc M,A) by XXREAL_2:def 4;
hence ((C_Meas M) . (A /\ E')) + ((C_Meas M) . (A /\ (X \ E'))) <= (C_Meas M) . A by Def10; :: thesis: verum

end;

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

end;

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