set G = D;
( {} c= union (rng D) & ( for n being Element of NAT holds D . n is Interval ) ) by FUNCOP_1:7;
then reconsider G = D as Interval_Covering of {} REAL by Def2;
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:13; :: thesis: verum

end;

hence F vol is nonnegative by SUPINF_2:39; :: 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: 0. is LowerBound of Svc A

proof

let x be ExtReal; :: 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;
set y = (Ser (F vol)) . 0;
F vol is nonnegative by A1;
then A5: 0. <= (Ser (F vol)) . 0 by SUPINF_2:40;
( SUM (F vol) = sup (rng (Ser (F vol))) & (Ser (F vol)) . 0 <= sup (rng (Ser (F vol))) ) by FUNCT_2:4, XXREAL_2:4;
hence 0. <= x by A4, A5, XXREAL_0:2; :: thesis: verum

end;

OS_Meas . A = inf (Svc A) by Def10;
hence 0. <= OS_Meas . A by A3, XXREAL_2:def 4; :: thesis: verum

end;

hence OS_Meas is nonnegative by MEASURE1:def 2; :: according to MEASURE4:def 1 :: thesis: ( OS_Meas is zeroed & ( 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 [:omega,(bool REAL):] holds OS_Meas . (union (rng b₃)) <= SUM (OS_Meas * b₃) ) ) ) ) )
A6: 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:7;
hence ( 0 <= n implies (G vol) . n = 0. ) by Def4, MEASURE5:10; :: thesis: verum

end;

then vol G = (Ser (G vol)) . 0 by A1, SUPINF_2:48
.= (G vol) . 0 by SUPINF_2:def 11
.= 0. by A6 ;
then A7: 0. in Svc ({} REAL) by Def8;
0. is LowerBound of Svc ({} REAL)

proof

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

end;

then inf (Svc ({} REAL)) = 0. by A7, 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 [:omega,(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 [:omega,(bool REAL):] holds OS_Meas . (union (rng b₁)) <= SUM (OS_Meas * b₁) ) ) )
assume A9: A c= B ; :: thesis: ( OS_Meas . A <= OS_Meas . B & ( for b₁ being Element of bool [:omega,(bool REAL):] holds OS_Meas . (union (rng b₁)) <= SUM (OS_Meas * b₁) ) )
A10: Svc B c= Svc A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Svc B or x in Svc A )
assume A11: 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
A12: x = vol F by A11, Def8;
B c= union (rng F) by Def2;
then ( ( for n being Element of NAT holds F . n is Interval ) & A c= union (rng F) ) by A9;
then reconsider G = F as Interval_Covering of A by Def2;
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;

then A13: SUM (F vol) <= SUM (G vol) by SUPINF_2:43;
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;

then SUM (G vol) <= SUM (F vol) by SUPINF_2:43;
then x = vol G by A12, A13, XXREAL_0:1;
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 A10, XXREAL_2:60; :: thesis: for b₁ being Element of bool [:omega,(bool REAL):] holds OS_Meas . (union (rng b₁)) <= SUM (OS_Meas * b₁)
let F be sequence of (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 A14: for n being Element of NAT holds Svc (F . n) <> {+infty} ; :: thesis: OS_Meas . (union (rng F)) <= SUM (OS_Meas * F)

A16: 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:15;
hence 0. <= (OS_Meas * F) . n by A2; :: thesis: verum

end;

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

proof

set y = inf (Svc (union (rng F)));
set x = sup (rng (Ser (OS_Meas * F)));
assume A18: not inf (Svc (union (rng F))) <= sup (rng (Ser (OS_Meas * F))) ; :: thesis: contradiction
0. <= (OS_Meas * F) . 0 by A16;
then A19: 0. <= (Ser (OS_Meas * F)) . 0 by SUPINF_2:def 11;
(Ser (OS_Meas * F)) . 0 <= sup (rng (Ser (OS_Meas * F))) by FUNCT_2:4, XXREAL_2:4;
then 0. <= sup (rng (Ser (OS_Meas * F))) by A19, XXREAL_0:2;
then consider eps being Real such that
A20: 0. < eps and
A21: (sup (rng (Ser (OS_Meas * F)))) + eps < inf (Svc (union (rng F))) by A18, XXREAL_3:49;
reconsider eps = eps as Element of ExtREAL by XXREAL_0:def 1;
consider E being sequence of ExtREAL such that
A22: for n being Nat holds 0. < E . n and
A23: SUM E < eps by A20, MEASURE6:4;
A24: (SUM (OS_Meas * F)) + (SUM E) <= (SUM (OS_Meas * F)) + eps by A23, XXREAL_3:36;
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) );
A25: 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]
A26: ( OS_Meas . (F . n) = inf (Svc (F . n)) & In (0,REAL) is Real ) by Def10;
Svc (F . n) <> {+infty} by A14;
then not Svc (F . n) c= {+infty} by ZFMISC_1:33;
then (Svc (F . n)) \ {+infty} <> {} by XBOOLE_1:37;
then consider x being object such that
A27: x in (Svc (F . n)) \ {+infty} by XBOOLE_0:def 1;
reconsider x = x as R_eal by A27;
not x in {+infty} by A27, XBOOLE_0:def 5;
then A28: x <> +infty by TARSKI:def 1;
x in Svc (F . n) by A27, XBOOLE_0:def 5;
then inf (Svc (F . n)) <= x by XXREAL_2:3;
then inf (Svc (F . n)) < +infty by A28, XXREAL_0:2, XXREAL_0:4;
then inf (Svc (F . n)) is Element of REAL by A2, A26, XXREAL_0:46;
then consider S being ExtReal such that
A29: S in Svc (F . n) and
A30: S < (inf (Svc (F . n))) + (E . n) by A22, MEASURE6:5;
consider FS being Interval_Covering of F . n such that
A31: S = vol FS by A29, Def8;
reconsider FS = FS as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8;
take FS ; :: thesis: S₁[n,FS]
thus S₁[n,FS] by A30, A31; :: thesis: verum

end;

consider FF being sequence of (Funcs (NAT,(bool REAL))) such that
A32: for n being Element of NAT holds S₁[n,FF . n] from FUNCT_2:sch 3(A25);
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
ex F0 being Interval_Covering of F . n st
( F0 = FF . n & vol F0 < (inf (Svc (F . n))) + (E . n) ) by A32;
hence FF . n is Interval_Covering of F . n ; :: thesis: verum

end;

then reconsider FF = FF as Interval_Covering of F by Def3;
A33: inf (Svc (union (rng F))) <= SUM (vol FF) by Th15;
defpred S₂[ Element of NAT , Element of ExtREAL ] means $2 = ((OS_Meas * F) . $1) + (E . $1);
A34: for n being Element of NAT ex y being Element of ExtREAL st S₂[n,y] ;
consider G0 being sequence of ExtREAL such that
A35: for n being Element of NAT holds S₂[n,G0 . n] from FUNCT_2:sch 3(A34);
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
( ex F0 being Interval_Covering of F . n st
( F0 = FF . n & vol F0 < (inf (Svc (F . n))) + (E . n) ) & (OS_Meas * F) . n = OS_Meas . (F . n) ) by A32, FUNCT_2:15;
then vol (FF . n) < ((OS_Meas * F) . n) + (E . n) by Def10;
then (vol FF) . n < ((OS_Meas * F) . n) + (E . n) by Def7;
hence (vol FF) . n <= G0 . n by A35; :: thesis: verum

end;

then A36: SUM (vol FF) <= SUM G0 by SUPINF_2:43;
for n being Element of NAT holds 0. <= E . n by A22;
then E is nonnegative by SUPINF_2:39;
then SUM G0 <= (SUM (OS_Meas * F)) + (SUM E) by A17, A35, Th4;
then SUM G0 <= (SUM (OS_Meas * F)) + eps by A24, XXREAL_0:2;
then SUM (vol FF) <= (SUM (OS_Meas * F)) + eps by A36, XXREAL_0:2;
hence contradiction by A21, A33, XXREAL_0:2; :: thesis: verum

end;

hence OS_Meas . (union (rng F)) <= SUM (OS_Meas * F) by 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
A37: Svc (F . n) = {+infty} ;
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:15;
hence 0. <= (OS_Meas * F) . n by A2; :: thesis: verum

end;

then A38: OS_Meas * F is nonnegative by SUPINF_2:39;
inf {+infty} = +infty by XXREAL_2:13;
then OS_Meas . (F . n) = +infty by A37, Def10;
then (OS_Meas * F) . n = +infty by FUNCT_2:15;
then SUM (OS_Meas * F) = +infty by A38, SUPINF_2:45;
hence OS_Meas . (union (rng F)) <= SUM (OS_Meas * F) by XXREAL_0:4; :: thesis: verum

end;

end;