let X be set ; :: thesis: for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
let F be Field_Subset of X; :: thesis: for M being Measure of F
for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
let M be Measure of F; :: thesis: for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
let Sets be SetSequence of X; :: thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

A1: now :: thesis: ( ( for n being Element of NAT holds Svc (M,(Sets . n)) <> {+infty} ) implies (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) )

assume A2: for n being Element of NAT holds Svc (M,(Sets . n)) <> {+infty} ; :: thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
inf (Svc (M,(union (rng Sets)))) <= sup (rng (Ser ((C_Meas M) * Sets)))

proof

set y = inf (Svc (M,(union (rng Sets))));
set x = sup (rng (Ser ((C_Meas M) * Sets)));
A3: (Ser ((C_Meas M) * Sets)) . 0 <= sup (rng (Ser ((C_Meas M) * Sets))) by FUNCT_2:4, XXREAL_2:4;
A4: (C_Meas M) * Sets is nonnegative by Th10, MEASURE1:25;
then 0 <= ((C_Meas M) * Sets) . 0 by SUPINF_2:39;
then A5: 0 <= (Ser ((C_Meas M) * Sets)) . 0 by SUPINF_2:def 11;
assume not inf (Svc (M,(union (rng Sets)))) <= sup (rng (Ser ((C_Meas M) * Sets))) ; :: thesis: contradiction
then consider eps being Real such that
A6: 0 < eps and
A7: (sup (rng (Ser ((C_Meas M) * Sets)))) + eps < inf (Svc (M,(union (rng Sets)))) by A5, A3, XXREAL_3:49;
consider E being sequence of ExtREAL such that
A8: for n being Nat holds 0 < E . n and
A9: SUM E < eps by A6, MEASURE6:4;
for n being Element of NAT holds 0 <= E . n by A8;
then A10: E is nonnegative by SUPINF_2:39;
defpred S₁[ Element of NAT , set ] means ex F0 being Covering of Sets . $1,F st
( $2 = F0 & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . $1)))) + (E . $1) );
A11: for n being Element of NAT ex F0 being Element of Funcs (NAT,(bool X)) st S₁[n,F0]

proof

let n be Element of NAT ; :: thesis: ex F0 being Element of Funcs (NAT,(bool X)) st S₁[n,F0]
( C_Meas M is nonnegative & (C_Meas M) . (Sets . n) = inf (Svc (M,(Sets . n))) ) by Def8, Th10;
then A12: ( 0 in REAL & 0. <= inf (Svc (M,(Sets . n))) ) by SUPINF_2:51, XREAL_0:def 1;
Svc (M,(Sets . n)) <> {+infty} by A2;
then not Svc (M,(Sets . n)) c= {+infty} by ZFMISC_1:33;
then (Svc (M,(Sets . n))) \ {+infty} <> {} by XBOOLE_1:37;
then consider x being object such that
A13: x in (Svc (M,(Sets . n))) \ {+infty} by XBOOLE_0:def 1;
reconsider x = x as R_eal by A13;
not x in {+infty} by A13, XBOOLE_0:def 5;
then A14: x <> +infty by TARSKI:def 1;
x in Svc (M,(Sets . n)) by A13, XBOOLE_0:def 5;
then inf (Svc (M,(Sets . n))) <= x by XXREAL_2:3;
then inf (Svc (M,(Sets . n))) < +infty by A14, XXREAL_0:2, XXREAL_0:4;
then inf (Svc (M,(Sets . n))) is Element of REAL by A12, XXREAL_0:46;
then consider S1 being ExtReal such that
A15: S1 in Svc (M,(Sets . n)) and
A16: S1 < (inf (Svc (M,(Sets . n)))) + (E . n) by A8, MEASURE6:5;
consider FS being Covering of Sets . n,F such that
A17: S1 = SUM (vol (M,FS)) by A15, Def7;
reconsider FS = FS as Element of Funcs (NAT,(bool X)) by FUNCT_2:8;
take FS ; :: thesis: S₁[n,FS]
thus S₁[n,FS] by A16, A17; :: thesis: verum

end;

consider FF being sequence of (Funcs (NAT,(bool X))) such that
A18: for n being Element of NAT holds S₁[n,FF . n] from FUNCT_2:sch 3(A11);
A19: for n being Nat holds FF . n is Covering of Sets . n,F

proof

let n be Nat; :: thesis: FF . n is Covering of Sets . n,F
n in NAT by ORDINAL1:def 12;
then ex F0 being Covering of Sets . n,F st
( F0 = FF . n & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . n)))) + (E . n) ) by A18;
hence FF . n is Covering of Sets . n,F ; :: thesis: verum

end;

deffunc H₁( Element of NAT ) -> Element of ExtREAL = (((C_Meas M) * Sets) . $1) + (E . $1);
A20: for x being Element of NAT holds H₁(x) is Element of ExtREAL ;
consider G0 being sequence of ExtREAL such that
A21: for n being Element of NAT holds G0 . n = H₁(n) from FUNCT_2:sch 9(A20);
reconsider FF = FF as Covering of Sets,F by A19, Def4;
for n being Element of NAT holds (Volume (M,FF)) . n <= G0 . n

proof

let n be Element of NAT ; :: thesis: (Volume (M,FF)) . n <= G0 . n
( ex F0 being Covering of Sets . n,F st
( F0 = FF . n & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . n)))) + (E . n) ) & ((C_Meas M) * Sets) . n = (C_Meas M) . (Sets . n) ) by A18, FUNCT_2:15;
then SUM (vol (M,(FF . n))) < (((C_Meas M) * Sets) . n) + (E . n) by Def8;
then (Volume (M,FF)) . n < (((C_Meas M) * Sets) . n) + (E . n) by Def6;
hence (Volume (M,FF)) . n <= G0 . n by A21; :: thesis: verum

end;

then A22: SUM (Volume (M,FF)) <= SUM G0 by SUPINF_2:43;

A23: now :: thesis: for n being Nat holds G0 . n = (((C_Meas M) * Sets) . n) + (E . n)

let n be Nat; :: thesis: G0 . n = (((C_Meas M) * Sets) . n) + (E . n)
n is Element of NAT by ORDINAL1:def 12;
hence G0 . n = (((C_Meas M) * Sets) . n) + (E . n) by A21; :: thesis: verum

end;

(SUM ((C_Meas M) * Sets)) + (SUM E) <= (SUM ((C_Meas M) * Sets)) + eps by A9, XXREAL_3:36;
then SUM G0 <= (SUM ((C_Meas M) * Sets)) + eps by A4, A10, A23, Th3;
then A24: SUM (Volume (M,FF)) <= (SUM ((C_Meas M) * Sets)) + eps by A22, XXREAL_0:2;
inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,FF)) by Th7;
hence contradiction by A7, A24, XXREAL_0:2; :: thesis: verum

end;

hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by Def8; :: thesis: verum

end;

now :: thesis: ( ex n being Element of NAT st Svc (M,(Sets . n)) = {+infty} implies (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) )

assume ex n being Element of NAT st Svc (M,(Sets . n)) = {+infty} ; :: thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
then consider n being Element of NAT such that
A25: Svc (M,(Sets . n)) = {+infty} ;
inf {+infty} = +infty by XXREAL_2:13;
then (C_Meas M) . (Sets . n) = +infty by A25, Def8;
hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by Lm2; :: thesis: verum

end;

hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by A1; :: thesis: verum