A1: for A being Subset of REAL
for F being Interval_Covering of A holds F vol is nonnegative

proof

let A be Subset of REAL ; :: thesis: for F being Interval_Covering of A holds F vol is nonnegative
let F be Interval_Covering of A; :: thesis: F vol is nonnegative
for n being Element of NAT holds 0. <= (F vol ) . n

proof

let n be Element of NAT ; :: thesis: 0. <= (F vol ) . n
(F vol ) . n = diameter (F . n) by Def4;
hence 0. <= (F vol ) . n by MEASURE5:63; :: thesis: verum

end;

hence F vol is nonnegative by SUPINF_2:58; :: thesis: verum

end;

A2: for A being Subset of REAL holds 0. <= OS_Meas . A

proof

let A be Subset of REAL ; :: thesis: 0. <= OS_Meas . A
A3: OS_Meas . A = inf (Svc A) by Def10;
0. is LowerBound of Svc A

proof

let x be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not x in Svc A or 0. <= x )
assume x in Svc A ; :: thesis: 0. <= x
then consider F being Interval_Covering of A such that
A4: x = vol F by Def8;
A5: F vol is nonnegative by A1;
A6: SUM (F vol ) = sup (rng (Ser (F vol ))) by SUPINF_2:def 23;
set y = (Ser (F vol )) . 0 ;
( 0. <= (Ser (F vol )) . 0 & (Ser (F vol )) . 0 <= sup (rng (Ser (F vol ))) ) by A5, FUNCT_2:6, SUPINF_2:59, XXREAL_2:4;
hence 0. <= x by A4, A6, XXREAL_0:2; :: thesis: verum

end;

hence 0. <= OS_Meas . A by A3, XXREAL_2:def 4; :: thesis: verum

end;

hence OS_Meas is nonnegative by MEASURE1:def 4; :: according to MEASURE4:def 2 :: thesis: ( OS_Meas is V65() & ( for b₁, b₂ being Element of bool REAL holds
( not b₁ c= b₂ or ( OS_Meas . b₁ <= OS_Meas . b₂ & ( for b₃ being Element of bool [:NAT ,(bool REAL ):] holds OS_Meas . (union (rng b₃)) <= SUM (OS_Meas * b₃) ) ) ) ) )
set G = D;
A7: {} c= union (rng D) by XBOOLE_1:2;
for n being Element of NAT holds D . n is Interval by FUNCOP_1:13;
then reconsider G = D as Interval_Covering of {} REAL by A7, Def2;
A9: for r being Element of NAT st 0 <= r holds
(G vol ) . r = 0.

proof

let n be Element of NAT ; :: thesis: ( 0 <= n implies (G vol ) . n = 0. )
diameter (G . n) = diameter {} by FUNCOP_1:13;
hence ( 0 <= n implies (G vol ) . n = 0. ) by Def4, MEASURE5:60; :: thesis: verum

end;

then vol G = (Ser (G vol )) . 0 by A1, SUPINF_2:67
.= (G vol ) . 0 by SUPINF_2:63
.= 0. by A9 ;
then A10: 0. in Svc ({} REAL ) by Def8;
0. is LowerBound of Svc ({} REAL )

proof

let x be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not x in Svc ({} REAL ) or 0. <= x )
assume A11: x in Svc ({} REAL ) ; :: thesis: 0. <= x
0. <= OS_Meas . ({} REAL ) by A2;
then ( 0. <= inf (Svc ({} REAL )) & inf (Svc ({} REAL )) <= x ) by A11, Def10, XXREAL_2:3;
hence 0. <= x by XXREAL_0:2; :: thesis: verum

end;

then inf (Svc ({} REAL )) = 0. by A10, XXREAL_2:56;
hence OS_Meas . {} = 0 by Def10; :: according to VALUED_0:def 19 :: thesis: for b₁, b₂ being Element of bool REAL holds
( not b₁ c= b₂ or ( OS_Meas . b₁ <= OS_Meas . b₂ & ( for b₃ being Element of bool [:NAT ,(bool REAL ):] holds OS_Meas . (union (rng b₃)) <= SUM (OS_Meas * b₃) ) ) )
let A, B be Subset of REAL ; :: thesis: ( not A c= B or ( OS_Meas . A <= OS_Meas . B & ( for b₁ being Element of bool [:NAT ,(bool REAL ):] holds OS_Meas . (union (rng b₁)) <= SUM (OS_Meas * b₁) ) ) )
assume A12: A c= B ; :: thesis: ( OS_Meas . A <= OS_Meas . B & ( for b₁ being Element of bool [:NAT ,(bool REAL ):] holds OS_Meas . (union (rng b₁)) <= SUM (OS_Meas * b₁) ) )
A13: Svc B c= Svc A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Svc B or x in Svc A )
assume A14: x in Svc B ; :: thesis: x in Svc A
then reconsider x = x as R_eal ;
consider F being Interval_Covering of B such that
A15: x = vol F by A14, Def8;
A16: ( B c= union (rng F) & ( for n being Element of NAT holds F . n is Interval ) ) by Def2;
then A c= union (rng F) by A12, XBOOLE_1:1;
then reconsider G = F as Interval_Covering of A by A16, Def2;
x = vol G

proof

A17: for n being Element of NAT holds (G vol ) . n <= (F vol ) . n

proof

let n be Element of NAT ; :: thesis: (G vol ) . n <= (F vol ) . n
(G vol ) . n = diameter (G . n) by Def4
.= (F vol ) . n by Def4 ;
hence (G vol ) . n <= (F vol ) . n ; :: thesis: verum

end;

A18: SUM (G vol ) <= SUM (F vol ) by A17, SUPINF_2:62;
A19: for n being Element of NAT holds (F vol ) . n <= (G vol ) . n

proof

let n be Element of NAT ; :: thesis: (F vol ) . n <= (G vol ) . n
(G vol ) . n = diameter (G . n) by Def4
.= (F vol ) . n by Def4 ;
hence (F vol ) . n <= (G vol ) . n ; :: thesis: verum

end;

SUM (F vol ) <= SUM (G vol ) by A19, SUPINF_2:62;
hence x = vol G by A15, A18, XXREAL_0:1; :: thesis: verum

end;

hence x in Svc A by Def8; :: thesis: verum

end;

( OS_Meas . A = inf (Svc A) & OS_Meas . B = inf (Svc B) ) by Def10;
hence OS_Meas . A <= OS_Meas . B by A13, XXREAL_2:60; :: thesis: for b₁ being Element of bool [:NAT ,(bool REAL ):] holds OS_Meas . (union (rng b₁)) <= SUM (OS_Meas * b₁)
let F be Function of NAT ,(bool REAL ); :: thesis: OS_Meas . (union (rng F)) <= SUM (OS_Meas * F)

per cases ( for n being Element of NAT holds Svc (F . n) <> {+infty } or ex n being Element of NAT st Svc (F . n) = {+infty } ) ;

suppose A20: for n being Element of NAT holds Svc (F . n) <> {+infty } ; :: thesis: OS_Meas . (union (rng F)) <= SUM (OS_Meas * F)

A21: SUM (OS_Meas * F) = sup (rng (Ser (OS_Meas * F))) by SUPINF_2:def 23;
A22: for n being Element of NAT holds 0. <= (OS_Meas * F) . n

proof

let n be Element of NAT ; :: thesis: 0. <= (OS_Meas * F) . n
(OS_Meas * F) . n = OS_Meas . (F . n) by FUNCT_2:21;
hence 0. <= (OS_Meas * F) . n by A2; :: thesis: verum

end;

then A23: OS_Meas * F is nonnegative by SUPINF_2:58;
inf (Svc (union (rng F))) <= sup (rng (Ser (OS_Meas * F)))

proof

assume A24: not inf (Svc (union (rng F))) <= sup (rng (Ser (OS_Meas * F))) ; :: thesis: contradiction
set y = inf (Svc (union (rng F)));
set x = sup (rng (Ser (OS_Meas * F)));
0. <= (OS_Meas * F) . 0 by A22;
then A25: 0. <= (Ser (OS_Meas * F)) . 0 by SUPINF_2:63;
(Ser (OS_Meas * F)) . 0 <= sup (rng (Ser (OS_Meas * F))) by FUNCT_2:6, XXREAL_2:4;
then 0. <= sup (rng (Ser (OS_Meas * F))) by A25, XXREAL_0:2;
then consider eps being real number such that
A26: ( 0. < eps & (sup (rng (Ser (OS_Meas * F)))) + eps < inf (Svc (union (rng F))) ) by A24, XXREAL_3:55;
reconsider eps = eps as Element of ExtREAL by XXREAL_0:def 1;
consider E being Function of NAT ,ExtREAL such that
A27: ( ( for n being Element of NAT holds 0. < E . n ) & SUM E < eps ) by A26, MEASURE6:31;
defpred S₁[ Element of NAT , set ] means ex F0 being Interval_Covering of F . $1 st
( $2 = F0 & vol F0 < (inf (Svc (F . $1))) + (E . $1) );
A28: for n being Element of NAT ex F0 being Element of Funcs NAT ,(bool REAL ) st S₁[n,F0]

proof

let n be Element of NAT ; :: thesis: ex F0 being Element of Funcs NAT ,(bool REAL ) st S₁[n,F0]
A29: ( OS_Meas . (F . n) = inf (Svc (F . n)) & 0. <= OS_Meas . (F . n) ) by A2, Def10;
Svc (F . n) <> {+infty } by A20;
then not Svc (F . n) c= {+infty } by ZFMISC_1:39;
then (Svc (F . n)) \ {+infty } <> {} by XBOOLE_1:37;
then consider x being set such that
A30: x in (Svc (F . n)) \ {+infty } by XBOOLE_0:def 1;
reconsider x = x as R_eal by A30;
A31: ( x in Svc (F . n) & not x in {+infty } ) by A30, XBOOLE_0:def 5;
then A32: ( x in Svc (F . n) & x <> +infty ) by TARSKI:def 1;
inf (Svc (F . n)) <= x by A31, XXREAL_2:3;
then ( 0 is Real & 0. <= inf (Svc (F . n)) & inf (Svc (F . n)) < +infty ) by A29, A32, XXREAL_0:2, XXREAL_0:4;
then ( 0. < E . n & inf (Svc (F . n)) is Real ) by A27, XXREAL_0:46;
then consider S being ext-real number such that
A33: ( S in Svc (F . n) & S < (inf (Svc (F . n))) + (E . n) ) by MEASURE6:32;
consider FS being Interval_Covering of F . n such that
A34: S = vol FS by A33, Def8;
reconsider FS = FS as Element of Funcs NAT ,(bool REAL ) by FUNCT_2:11;
take FS ; :: thesis: S₁[n,FS]
thus S₁[n,FS] by A33, A34; :: thesis: verum

end;

consider FF being Function of NAT ,(Funcs NAT ,(bool REAL )) such that
A35: for n being Element of NAT holds S₁[n,FF . n] from FUNCT_2:sch 3(A28);
for n being Element of NAT holds FF . n is Interval_Covering of F . n

proof

let n be Element of NAT ; :: thesis: FF . n is Interval_Covering of F . n
consider F0 being Interval_Covering of F . n such that
A36: ( F0 = FF . n & vol F0 < (inf (Svc (F . n))) + (E . n) ) by A35;
thus FF . n is Interval_Covering of F . n by A36; :: thesis: verum

end;

then reconsider FF = FF as Interval_Covering of F by Def3;
for n being Element of NAT holds 0. <= E . n by A27;
then A37: E is nonnegative by SUPINF_2:58;
defpred S₂[ Element of NAT , Element of ExtREAL ] means $2 = ((OS_Meas * F) . $1) + (E . $1);
A38: for n being Element of NAT ex y being Element of ExtREAL st S₂[n,y] ;
consider G0 being Function of NAT ,ExtREAL such that
A39: for n being Element of NAT holds S₂[n,G0 . n] from FUNCT_2:sch 3(A38);
A40: SUM G0 <= (SUM (OS_Meas * F)) + (SUM E) by A23, A37, A39, Th4;
A41: for n being Element of NAT holds (vol FF) . n <= G0 . n

proof

let n be Element of NAT ; :: thesis: (vol FF) . n <= G0 . n
consider F0 being Interval_Covering of F . n such that
A42: ( F0 = FF . n & vol F0 < (inf (Svc (F . n))) + (E . n) ) by A35;
(OS_Meas * F) . n = OS_Meas . (F . n) by FUNCT_2:21;
then vol (FF . n) < ((OS_Meas * F) . n) + (E . n) by A42, Def10;
then (vol FF) . n < ((OS_Meas * F) . n) + (E . n) by Def7;
hence (vol FF) . n <= G0 . n by A39; :: thesis: verum

end;

A43: SUM (vol FF) <= SUM G0 by A41, SUPINF_2:62;
(SUM (OS_Meas * F)) + (SUM E) <= (SUM (OS_Meas * F)) + eps by A27, XXREAL_3:38;
then SUM G0 <= (SUM (OS_Meas * F)) + eps by A40, XXREAL_0:2;
then A44: SUM (vol FF) <= (SUM (OS_Meas * F)) + eps by A43, XXREAL_0:2;
inf (Svc (union (rng F))) <= SUM (vol FF) by Th16;
hence contradiction by A21, A26, A44, XXREAL_0:2; :: thesis: verum

end;

hence OS_Meas . (union (rng F)) <= SUM (OS_Meas * F) by A21, Def10; :: thesis: verum

end;

suppose ex n being Element of NAT st Svc (F . n) = {+infty } ; :: thesis: OS_Meas . (union (rng F)) <= SUM (OS_Meas * F)

then consider n being Element of NAT such that
A45: Svc (F . n) = {+infty } ;
inf {+infty } = +infty by XXREAL_2:13;
then OS_Meas . (F . n) = +infty by A45, Def10;
then A46: (OS_Meas * F) . n = +infty by FUNCT_2:21;
for n being Element of NAT holds 0. <= (OS_Meas * F) . n

proof

let n be Element of NAT ; :: thesis: 0. <= (OS_Meas * F) . n
(OS_Meas * F) . n = OS_Meas . (F . n) by FUNCT_2:21;
hence 0. <= (OS_Meas * F) . n by A2; :: thesis: verum

end;

then OS_Meas * F is nonnegative by SUPINF_2:58;
then SUM (OS_Meas * F) = +infty by A46, SUPINF_2:64;
hence OS_Meas . (union (rng F)) <= SUM (OS_Meas * F) by XXREAL_0:4; :: thesis: verum

end;

end;