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 () . (union (rng Sets)) <= SUM (() * Sets)

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

let M be Measure of F; :: thesis: for Sets being SetSequence of X holds () . (union (rng Sets)) <= SUM (() * Sets)
let Sets be SetSequence of X; :: thesis: () . (union (rng Sets)) <= SUM (() * Sets)
A1: now :: thesis: ( ( for n being Element of NAT holds Svc (M,(Sets . n)) <> ) implies () . (union (rng Sets)) <= SUM (() * Sets) )
assume A2: for n being Element of NAT holds Svc (M,(Sets . n)) <> ; :: thesis: () . (union (rng Sets)) <= SUM (() * Sets)
inf (Svc (M,(union (rng Sets)))) <= sup (rng (Ser (() * Sets)))
proof
set y = inf (Svc (M,(union (rng Sets))));
set x = sup (rng (Ser (() * Sets)));
A3: (Ser (() * Sets)) . 0 <= sup (rng (Ser (() * Sets))) by ;
A4: (C_Meas M) * Sets is nonnegative by ;
then 0 <= (() * Sets) . 0 by SUPINF_2:39;
then A5: 0 <= (Ser (() * Sets)) . 0 by SUPINF_2:def 11;
assume not inf (Svc (M,(union (rng Sets)))) <= sup (rng (Ser (() * Sets))) ; :: thesis: contradiction
then consider eps being Real such that
A6: 0 < eps and
A7: (sup (rng (Ser (() * Sets)))) + eps < inf (Svc (M,(union (rng Sets)))) by ;
consider E being sequence of ExtREAL such that
A8: for n being Nat holds 0 < E . n and
A9: SUM E < eps by ;
for n being Element of NAT holds 0 <= E . n by A8;
then A10: E is nonnegative by SUPINF_2:39;
defpred S1[ 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 S1[n,F0]
proof
let n be Element of NAT ; :: thesis: ex F0 being Element of Funcs (NAT,(bool X)) st S1[n,F0]
( C_Meas M is nonnegative & () . (Sets . n) = inf (Svc (M,(Sets . n))) ) by ;
then A12: ( 0 in REAL & 0. <= inf (Svc (M,(Sets . n))) ) by ;
Svc (M,(Sets . n)) <> by A2;
then not Svc (M,(Sets . n)) c= by ZFMISC_1:33;
then (Svc (M,(Sets . n))) \ <> {} by XBOOLE_1:37;
then consider x being object such that
A13: x in (Svc (M,(Sets . n))) \ by XBOOLE_0:def 1;
reconsider x = x as R_eal by A13;
not x in by ;
then A14: x <> +infty by TARSKI:def 1;
x in Svc (M,(Sets . n)) by ;
then inf (Svc (M,(Sets . n))) <= x by XXREAL_2:3;
then inf (Svc (M,(Sets . n))) < +infty by ;
then inf (Svc (M,(Sets . n))) is Element of REAL by ;
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 ;
consider FS being Covering of Sets . n,F such that
A17: S1 = SUM (vol (M,FS)) by ;
reconsider FS = FS as Element of Funcs (NAT,(bool X)) by FUNCT_2:8;
take FS ; :: thesis: S1[n,FS]
thus S1[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 S1[n,FF . n] from 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 H1( Element of NAT ) -> object = ((() * Sets) . \$1) + (E . \$1);
A20: for x being Element of NAT holds H1(x) is Element of ExtREAL by XXREAL_0:def 1;
consider G0 being sequence of ExtREAL such that
A21: for n being Element of NAT holds G0 . n = H1(n) from reconsider FF = FF as Covering of Sets,F by ;
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) ) & (() * Sets) . n = () . (Sets . n) ) by ;
then SUM (vol (M,(FF . n))) < ((() * Sets) . n) + (E . n) by Def8;
then (Volume (M,FF)) . n < ((() * 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 = ((() * Sets) . n) + (E . n)
let n be Nat; :: thesis: G0 . n = ((() * Sets) . n) + (E . n)
n is Element of NAT by ORDINAL1:def 12;
hence G0 . n = ((() * Sets) . n) + (E . n) by A21; :: thesis: verum
end;
(SUM (() * Sets)) + (SUM E) <= (SUM (() * Sets)) + eps by ;
then SUM G0 <= (SUM (() * Sets)) + eps by A4, A10, A23, Th3;
then A24: SUM (Volume (M,FF)) <= (SUM (() * Sets)) + eps by ;
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 (() * Sets) by Def8; :: thesis: verum
end;
now :: thesis: ( ex n being Element of NAT st Svc (M,(Sets . n)) = implies () . (union (rng Sets)) <= SUM (() * Sets) )
assume ex n being Element of NAT st Svc (M,(Sets . n)) = ; :: thesis: () . (union (rng Sets)) <= SUM (() * Sets)
then consider n being Element of NAT such that
A25: Svc (M,(Sets . n)) = ;
inf = +infty by XXREAL_2:13;
then (C_Meas M) . (Sets . n) = +infty by ;
hence (C_Meas M) . (union (rng Sets)) <= SUM (() * Sets) by Lm2; :: thesis: verum
end;
hence (C_Meas M) . (union (rng Sets)) <= SUM (() * Sets) by A1; :: thesis: verum