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

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:6, XXREAL_2:4;
A4: (C_Meas M) * Sets is nonnegative by Th10, MEASURE1:54;
then 0 <= ((C_Meas M) * Sets) . 0 by SUPINF_2:58;
then A5: 0 <= (Ser ((C_Meas M) * Sets)) . 0 by SUPINF_2:63;
assume not inf (Svc M,(union (rng Sets))) <= sup (rng (Ser ((C_Meas M) * Sets))) ; :: thesis: contradiction
then consider eps being real number 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:55;
eps in ExtREAL by XXREAL_0:def 1;
then consider E being Function of NAT ,ExtREAL such that
A8: for n being Element of NAT holds 0 < E . n and
A9: SUM E < eps by A6, MEASURE6:31;
for n being Element of NAT holds 0 <= E . n by A8;
then A10: E is nonnegative by SUPINF_2:58;
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 is Real & 0. <= inf (Svc M,(Sets . n)) ) by SUPINF_2:70;
Svc M,(Sets . n) <> {+infty } by A2;
then not Svc M,(Sets . n) c= {+infty } by ZFMISC_1:39;
then (Svc M,(Sets . n)) \ {+infty } <> {} by XBOOLE_1:37;
then consider x being set 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 Real by A12, XXREAL_0:46;
then consider S1 being ext-real number such that
A15: S1 in Svc M,(Sets . n) and
A16: S1 < (inf (Svc M,(Sets . n))) + (E . n) by A8, MEASURE6:32;
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:11;
take FS ; :: thesis: S₁[n,FS]
thus S₁[n,FS] by A16, A17; :: thesis: verum

end;

consider FF being Function of NAT ,(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 13;
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 ) -> set = (((C_Meas M) * Sets) . $1) + (E . $1);
A20: for x being Element of NAT holds H₁(x) is Element of ExtREAL by XXREAL_0:def 1;
consider G0 being Function of NAT ,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:21;
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:62;

A23: now

let n be Nat; :: thesis: G0 . n = (((C_Meas M) * Sets) . n) + (E . n)
n is Element of NAT by ORDINAL1:def 13;
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:38;
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

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