:: MEASURE7 semantic presentation

begin

theorem Th1: :: MEASURE7:1
for F being Function of NAT,ExtREAL st ( for n being Element of NAT holds F . n = 0. ) holds
SUM F = 0.
proof
let F be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds F . n = 0. ) implies SUM F = 0. )
defpred S1[ Element of NAT ] means (Ser F) . $1 = 0. ;
assume A1: for n being Element of NAT holds F . n = 0. ; ::_thesis: SUM F = 0.
A2: for t being Element of NAT st S1[t] holds
S1[t + 1]
proof
let t be Element of NAT ; ::_thesis: ( S1[t] implies S1[t + 1] )
assume  (Ser F) . t = 0. ; ::_thesis: S1[t + 1]
hence (Ser F) . (t + 1) = 0. + (F . (t + 1)) by SUPINF_2:44
.= F . (t + 1) by XXREAL_3:4
.= 0. by A1 ;
::_thesis: verum
end;
A3: (Ser F) . 0 = F . 0 by SUPINF_2:44
.= 0. by A1 ;
then A4: S1[ 0 ] ;
A5: for s being Element of NAT holds S1[s] from NAT_1:sch_1(A4, A2);
A6: rng (Ser F) = {0.}
proof
thus  rng (Ser F) c= {0.} :: according to XBOOLE_0:def_10 ::_thesis: {0.} c= rng (Ser F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Ser F) or x in {0.} )
assume  x in rng (Ser F) ; ::_thesis: x in {0.}
then consider s being set  such that
A7: s in dom (Ser F) and
A8: x = (Ser F) . s by FUNCT_1:def_3;
reconsider s = s as Element of NAT by A7;
 (Ser F) . s = 0. by A5;
hence  x in {0.} by A8, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {0.} or x in rng (Ser F) )
assume  x in {0.} ; ::_thesis: x in rng (Ser F)
then  ( dom (Ser F) = NAT & x = 0. ) by FUNCT_2:def_1, TARSKI:def_1;
hence  x in rng (Ser F) by A3, FUNCT_1:def_3; ::_thesis: verum
end;
 sup {0.} = 0. by XXREAL_2:11;
hence  SUM F = 0. by A6, SUPINF_2:def_17; ::_thesis: verum
end;

theorem Th2: :: MEASURE7:2
for F being Function of NAT,ExtREAL st F is V93() holds
for n being Element of NAT holds F . n <= (Ser F) . n
proof
let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies for n being Element of NAT holds F . n <= (Ser F) . n )
assume A1: F is V93() ; ::_thesis: for n being Element of NAT holds F . n <= (Ser F) . n
let n be Element of NAT ; ::_thesis: F . n <= (Ser F) . n
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: F . n <= (Ser F) . n
hence  F . n <= (Ser F) . n by SUPINF_2:44; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: F . n <= (Ser F) . n
then consider k being Nat such that
A2: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A3: 0. <= (Ser F) . k by A1, SUPINF_2:40;
 (Ser F) . n = ((Ser F) . k) + (F . n) by A2, SUPINF_2:44;
then  0. + (F . n) <= (Ser F) . n by A3, XXREAL_3:36;
hence  F . n <= (Ser F) . n by XXREAL_3:4; ::_thesis: verum
end;
end;
end;

theorem Th3: :: MEASURE7:3
for F, G, H being Function of NAT,ExtREAL st G is V93() & H is V93() & ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) holds
for n being Element of NAT holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n)
proof
let F, G, H be Function of NAT,ExtREAL; ::_thesis: ( G is V93() & H is V93() & ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) implies for n being Element of NAT holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n) )
assume that
A1: G is V93() and
A2: H is V93() ; ::_thesis: ( ex n being Element of NAT st not F . n = (G . n) + (H . n) or for n being Element of NAT holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n) )
defpred S1[ Element of NAT ] means (Ser F) . $1 = ((Ser G) . $1) + ((Ser H) . $1);
assume A3: for n being Element of NAT holds F . n = (G . n) + (H . n) ; ::_thesis: for n being Element of NAT holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n)
A4: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: (Ser F) . k = ((Ser G) . k) + ((Ser H) . k) ; ::_thesis: S1[k + 1]
set n = k + 1;
A6: ( (Ser G) . (k + 1) = ((Ser G) . k) + (G . (k + 1)) & (Ser H) . (k + 1) = ((Ser H) . k) + (H . (k + 1)) ) by SUPINF_2:44;
A7: 0. <= H . (k + 1) by A2, SUPINF_2:39;
A8: ( F . (k + 1) = (G . (k + 1)) + (H . (k + 1)) & 0. <= G . (k + 1) ) by A1, A3, SUPINF_2:39;
A9: 0. <= (Ser G) . k by A1, SUPINF_2:40;
A10: 0. <= (Ser G) . (k + 1) by A1, SUPINF_2:40;
A11: 0. <= (Ser H) . k by A2, SUPINF_2:40;
 ( 0. <= G . (k + 1) & 0. <= H . (k + 1) ) by A1, A2, SUPINF_2:39;
then  0. + 0. <= (G . (k + 1)) + (H . (k + 1)) by XXREAL_3:36;
then  0. <= F . (k + 1) by A3;
then (((Ser G) . k) + ((Ser H) . k)) + (F . (k + 1)) = (((Ser G) . k) + (F . (k + 1))) + ((Ser H) . k) by A9, A11, XXREAL_3:44
.= ((((Ser G) . k) + (G . (k + 1))) + (H . (k + 1))) + ((Ser H) . k) by A9, A7, A8, XXREAL_3:44
.= ((Ser G) . (k + 1)) + ((Ser H) . (k + 1)) by A6, A11, A10, A7, XXREAL_3:44 ;
hence  S1[k + 1] by A5, SUPINF_2:44; ::_thesis: verum
end;
A12: (Ser H) . 0 = H . 0 by SUPINF_2:44;
 ( (Ser F) . 0 = F . 0 & (Ser G) . 0 = G . 0 ) by SUPINF_2:44;
then A13: S1[ 0 ] by A3, A12;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A13, A4); ::_thesis: verum
end;

theorem Th4: :: MEASURE7:4
for F, G, H being Function of NAT,ExtREAL st ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) & G is V93() & H is V93() holds
SUM F <= (SUM G) + (SUM H)
proof
let F, G, H be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) & G is V93() & H is V93() implies SUM F <= (SUM G) + (SUM H) )
assume A1: for n being Element of NAT holds F . n = (G . n) + (H . n) ; ::_thesis: ( not G is V93() or not H is V93() or SUM F <= (SUM G) + (SUM H) )
defpred S1[ Element of NAT ] means (Ser F) . $1 = ((Ser G) . $1) + ((Ser H) . $1);
assume that
A2: G is V93() and
A3: H is V93() ; ::_thesis: SUM F <= (SUM G) + (SUM H)
A4: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A5: ( (Ser G) . (k + 1) = ((Ser G) . k) + (G . (k + 1)) & (Ser H) . (k + 1) = ((Ser H) . k) + (H . (k + 1)) ) by SUPINF_2:44;
A6: 0. <= (Ser G) . k by A2, SUPINF_2:40;
A7: 0. <= (Ser H) . (k + 1) by A3, SUPINF_2:40;
A8: 0. <= H . (k + 1) by A3, SUPINF_2:39;
A9: 0. <= (Ser H) . k by A3, SUPINF_2:40;
 ( 0. <= G . (k + 1) & 0. <= H . (k + 1) ) by A2, A3, SUPINF_2:39;
then  0. + 0. <= (G . (k + 1)) + (H . (k + 1)) by XXREAL_3:36;
then A10: ( (Ser F) . (k + 1) = ((Ser F) . k) + (F . (k + 1)) & 0. <= F . (k + 1) ) by A1, SUPINF_2:44;
A11: 0. <= G . (k + 1) by A2, SUPINF_2:39;
assume  (Ser F) . k = ((Ser G) . k) + ((Ser H) . k) ; ::_thesis: S1[k + 1]
hence (Ser F) . (k + 1) = ((Ser G) . k) + (((Ser H) . k) + (F . (k + 1))) by A10, A6, A9, XXREAL_3:44
.= ((Ser G) . k) + (((Ser H) . k) + ((G . (k + 1)) + (H . (k + 1)))) by A1
.= ((Ser G) . k) + ((((Ser H) . k) + (H . (k + 1))) + (G . (k + 1))) by A11, A9, A8, XXREAL_3:44
.= ((Ser G) . (k + 1)) + ((Ser H) . (k + 1)) by A5, A6, A11, A7, XXREAL_3:44 ;
::_thesis: verum
end;
A12: (Ser H) . 0 = H . 0 by SUPINF_2:44;
 ( (Ser F) . 0 = F . 0 & (Ser G) . 0 = G . 0 ) by SUPINF_2:44;
then A13: S1[ 0 ] by A1, A12;
A14: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A4);
 (SUM G) + (SUM H) is UpperBound of rng (Ser F)
proof
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not x in rng (Ser F) or x <= (SUM G) + (SUM H) )
A15: dom (Ser F) = NAT by FUNCT_2:def_1;
assume  x in rng (Ser F) ; ::_thesis: x <= (SUM G) + (SUM H)
then consider n being set  such that
A16: n in NAT and
A17: x = (Ser F) . n by A15, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A16;
 (Ser H) . n <= sup (rng (Ser H)) by FUNCT_2:4, XXREAL_2:4;
then A18: (Ser H) . n <= SUM H by SUPINF_2:def_17;
 (Ser G) . n <= sup (rng (Ser G)) by FUNCT_2:4, XXREAL_2:4;
then  (Ser G) . n <= SUM G by SUPINF_2:def_17;
then  ((Ser G) . n) + ((Ser H) . n) <= (SUM G) + (SUM H) by A18, XXREAL_3:36;
hence  x <= (SUM G) + (SUM H) by A14, A17; ::_thesis: verum
end;
then  sup (rng (Ser F)) <= (SUM G) + (SUM H) by XXREAL_2:def_3;
hence  SUM F <= (SUM G) + (SUM H) by SUPINF_2:def_17; ::_thesis: verum
end;

theorem Th5: :: MEASURE7:5
for F, G being Function of NAT,ExtREAL st ( for n being Element of NAT holds F . n <= G . n ) holds
for n being Element of NAT holds (Ser F) . n <= SUM G
proof
let F, G be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds F . n <= G . n ) implies for n being Element of NAT holds (Ser F) . n <= SUM G )
assume A1: for n being Element of NAT holds F . n <= G . n ; ::_thesis: for n being Element of NAT holds (Ser F) . n <= SUM G
let n be Element of NAT ; ::_thesis: (Ser F) . n <= SUM G
set y = (Ser G) . n;
 dom (Ser G) = NAT by FUNCT_2:def_1;
then  ( SUM G = sup (rng (Ser G)) & (Ser G) . n in rng (Ser G) ) by FUNCT_1:def_3, SUPINF_2:def_17;
hence  (Ser F) . n <= SUM G by A1, SUPINF_2:42, XXREAL_2:61; ::_thesis: verum
end;

theorem Th6: :: MEASURE7:6
for F being Function of NAT,ExtREAL st F is V93() holds
for n being Element of NAT holds (Ser F) . n <= SUM F
proof
let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies for n being Element of NAT holds (Ser F) . n <= SUM F )
 for n being Element of NAT holds F . n <= F . n ;
hence  ( F is V93() implies for n being Element of NAT holds (Ser F) . n <= SUM F ) by Th5; ::_thesis: verum
end;

definition
let S be non empty set ;
let H be Function of S,ExtREAL;
func On H ->  Function of NAT,ExtREAL means :Def1: :: MEASURE7:def 1
 for n being Element of NAT holds
( ( n in S implies it . n = H . n ) & ( not n in S implies it . n = 0. ) );
existence
 ex b1 being Function of NAT,ExtREAL st
for n being Element of NAT holds
( ( n in S implies b1 . n = H . n ) & ( not n in S implies b1 . n = 0. ) )
proof
defpred S1[ Element of NAT , Element of ExtREAL ] means ( ( $1 in S implies $2 = H . $1 ) & ( not $1 in S implies $2 = 0. ) );
A1: for n being Element of NAT ex y being Element of ExtREAL st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of ExtREAL st S1[n,y]
percases ( n in S or not n in S ) ;
suppose n in S ; ::_thesis: ex y being Element of ExtREAL st S1[n,y]
then reconsider n = n as Element of S ;
take  H . n ; ::_thesis: S1[n,H . n]
thus  S1[n,H . n] ; ::_thesis: verum
end;
supposeA2: not n in S ; ::_thesis: ex y being Element of ExtREAL st S1[n,y]
take  0. ; ::_thesis: S1[n, 0. ]
thus  S1[n, 0. ] by A2; ::_thesis: verum
end;
end;
end;
consider GG being Function of NAT,ExtREAL such that
A3: for n being Element of NAT holds S1[n,GG . n] from FUNCT_2:sch_3(A1);
take  GG ; ::_thesis: for n being Element of NAT holds
( ( n in S implies GG . n = H . n ) & ( not n in S implies GG . n = 0. ) )
thus  for n being Element of NAT holds
( ( n in S implies GG . n = H . n ) & ( not n in S implies GG . n = 0. ) ) by A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds
( ( n in S implies b1 . n = H . n ) & ( not n in S implies b1 . n = 0. ) ) ) & ( for n being Element of NAT holds
( ( n in S implies b2 . n = H . n ) & ( not n in S implies b2 . n = 0. ) ) ) holds
b1 = b2
proof
let G1, G2 be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds
( ( n in S implies G1 . n = H . n ) & ( not n in S implies G1 . n = 0. ) ) ) & ( for n being Element of NAT holds
( ( n in S implies G2 . n = H . n ) & ( not n in S implies G2 . n = 0. ) ) ) implies G1 = G2 )
assume that
A4: for n being Element of NAT holds
( ( n in S implies G1 . n = H . n ) & ( not n in S implies G1 . n = 0. ) ) and
A5: for n being Element of NAT holds
( ( n in S implies G2 . n = H . n ) & ( not n in S implies G2 . n = 0. ) ) ; ::_thesis: G1 = G2
 for n being set st n in NAT holds
G1 . n = G2 . n
proof
let n be set ; ::_thesis: ( n in NAT implies G1 . n = G2 . n )
assume  n in NAT ; ::_thesis: G1 . n = G2 . n
then reconsider n = n as Element of NAT ;
percases ( n in S or not n in S ) ;
supposeA6: n in S ; ::_thesis: G1 . n = G2 . n
then  G1 . n = H . n by A4;
hence  G1 . n = G2 . n by A5, A6; ::_thesis: verum
end;
supposeA7: not n in S ; ::_thesis: G1 . n = G2 . n
then  G1 . n = 0. by A4;
hence  G1 . n = G2 . n by A5, A7; ::_thesis: verum
end;
end;
end;
hence  G1 = G2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines On MEASURE7:def_1_:_
 for S being non empty set
for H being Function of S,ExtREAL
for b3 being Function of NAT,ExtREAL holds
( b3 = On H iff for n being Element of NAT holds
( ( n in S implies b3 . n = H . n ) & ( not n in S implies b3 . n = 0. ) ) );

theorem Th7: :: MEASURE7:7
for X being non empty set
for G being Function of X,ExtREAL st G is V93() holds
On G is V93()
proof
let X be non empty set ; ::_thesis: for G being Function of X,ExtREAL st G is V93() holds
On G is V93()
let G be Function of X,ExtREAL; ::_thesis: ( G is V93() implies On G is V93() )
assume A1: G is V93() ; ::_thesis: On G is V93()
 for n being Element of NAT holds 0. <= (On G) . n
proof
let n be Element of NAT ; ::_thesis: 0. <= (On G) . n
percases ( n in X or not n in X ) ;
supposeA2: n in X ; ::_thesis: 0. <= (On G) . n
then  (On G) . n = G . n by Def1;
hence  0. <= (On G) . n by A1, A2, SUPINF_2:39; ::_thesis: verum
end;
suppose not n in X ; ::_thesis: 0. <= (On G) . n
hence  0. <= (On G) . n by Def1; ::_thesis: verum
end;
end;
end;
hence  On G is V93() by SUPINF_2:39; ::_thesis: verum
end;

theorem Th8: :: MEASURE7:8
for F being Function of NAT,ExtREAL st F is V93() holds
for n, k being Element of NAT st n <= k holds
(Ser F) . n <= (Ser F) . k
proof
let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies for n, k being Element of NAT st n <= k holds
(Ser F) . n <= (Ser F) . k )
assume A1: F is V93() ; ::_thesis: for n, k being Element of NAT st n <= k holds
(Ser F) . n <= (Ser F) . k
let n, k be Element of NAT ; ::_thesis: ( n <= k implies (Ser F) . n <= (Ser F) . k )
defpred S1[ Element of NAT ] means (Ser F) . n <= (Ser F) . (n + $1);
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: (Ser F) . n <= (Ser F) . (n + k) ; ::_thesis: S1[k + 1]
 (Ser F) . (n + k) <= (Ser F) . ((n + k) + 1) by A1, SUPINF_2:40;
hence  S1[k + 1] by A3, XXREAL_0:2; ::_thesis: verum
end;
assume  n <= k ; ::_thesis: (Ser F) . n <= (Ser F) . k
then consider s being Nat such that
A4: k = n + s by NAT_1:10;
reconsider s = s as Element of NAT by ORDINAL1:def_12;
A5: k = n + s by A4;
A6: S1[ 0 ] ;
 for s being Element of NAT holds S1[s] from NAT_1:sch_1(A6, A2);
hence  (Ser F) . n <= (Ser F) . k by A5; ::_thesis: verum
end;

theorem Th9: :: MEASURE7:9
for k being Element of NAT
for F being Function of NAT,ExtREAL st ( for n being Element of NAT st n <> k holds
F . n = 0. ) holds
( ( for n being Element of NAT st n < k holds
(Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds
(Ser F) . n = F . k ) )
proof
let k be Element of NAT ; ::_thesis: for F being Function of NAT,ExtREAL st ( for n being Element of NAT st n <> k holds
F . n = 0. ) holds
( ( for n being Element of NAT st n < k holds
(Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds
(Ser F) . n = F . k ) )
let F be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT st n <> k holds
F . n = 0. ) implies ( ( for n being Element of NAT st n < k holds
(Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds
(Ser F) . n = F . k ) ) )
defpred S1[ Element of NAT ] means ( $1 < k implies (Ser F) . $1 = 0. );
assume A1: for n being Element of NAT st n <> k holds
F . n = 0. ; ::_thesis: ( ( for n being Element of NAT st n < k holds
(Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds
(Ser F) . n = F . k ) )
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: ( n < k implies (Ser F) . n = 0. ) ; ::_thesis: S1[n + 1]
assume A4: n + 1 < k ; ::_thesis: (Ser F) . (n + 1) = 0.
then A5: ( n <= n + 1 & F . (n + 1) = 0. ) by A1, NAT_1:11;
(Ser F) . (n + 1) = ((Ser F) . n) + (F . (n + 1)) by SUPINF_2:44
.= 0. by A3, A4, A5, XXREAL_0:2, XXREAL_3:4 ;
hence  (Ser F) . (n + 1) = 0. ; ::_thesis: verum
end;
A6: S1[ 0 ]
proof
assume  0 < k ; ::_thesis: (Ser F) . 0 = 0.
then  F . 0 = 0. by A1;
hence  (Ser F) . 0 = 0. by SUPINF_2:44; ::_thesis: verum
end;
A7: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A2);
defpred S2[ Element of NAT ] means ( k <= $1 implies (Ser F) . $1 = F . k );
A8: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A9: ( k <= n implies (Ser F) . n = F . k ) ; ::_thesis: S2[n + 1]
assume A10: k <= n + 1 ; ::_thesis: (Ser F) . (n + 1) = F . k
percases ( k <= n or k = n + 1 ) by A10, NAT_1:8;
supposeA11: k <= n ; ::_thesis: (Ser F) . (n + 1) = F . k
then  k <> n + 1 by NAT_1:13;
then A12: F . (n + 1) = 0. by A1;
(Ser F) . (n + 1) = ((Ser F) . n) + (F . (n + 1)) by SUPINF_2:44
.= F . k by A9, A11, A12, XXREAL_3:4 ;
hence  (Ser F) . (n + 1) = F . k ; ::_thesis: verum
end;
supposeA13: k = n + 1 ; ::_thesis: (Ser F) . (n + 1) = F . k
then  n < k by NAT_1:13;
then A14: (Ser F) . n = 0. by A7;
(Ser F) . (n + 1) = ((Ser F) . n) + (F . (n + 1)) by SUPINF_2:44
.= F . k by A13, A14, XXREAL_3:4 ;
hence  (Ser F) . (n + 1) = F . k ; ::_thesis: verum
end;
end;
end;
A15: S2[ 0 ]
proof
A16: 0 <= k by NAT_1:2;
assume  k <= 0 ; ::_thesis: (Ser F) . 0 = F . k
then  F . 0 = F . k by A16, XXREAL_0:1;
hence  (Ser F) . 0 = F . k by SUPINF_2:44; ::_thesis: verum
end;
 for n being Element of NAT holds S2[n] from NAT_1:sch_1(A15, A8);
hence  ( ( for n being Element of NAT st n < k holds
(Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds
(Ser F) . n = F . k ) ) by A7; ::_thesis: verum
end;

theorem Th10: :: MEASURE7:10
for G being Function of NAT,ExtREAL st G is V93() holds
for S being non empty Subset of NAT
for H being Function of S,NAT st H is one-to-one holds
SUM (On (G * H)) <= SUM G
proof
let G be Function of NAT,ExtREAL; ::_thesis: ( G is V93() implies for S being non empty Subset of NAT
for H being Function of S,NAT st H is one-to-one holds
SUM (On (G * H)) <= SUM G )
assume A1: G is V93() ; ::_thesis: for S being non empty Subset of NAT
for H being Function of S,NAT st H is one-to-one holds
SUM (On (G * H)) <= SUM G
let S be non empty Subset of NAT; ::_thesis: for H being Function of S,NAT st H is one-to-one holds
SUM (On (G * H)) <= SUM G
let H be Function of S,NAT; ::_thesis: ( H is one-to-one implies SUM (On (G * H)) <= SUM G )
defpred S1[ Element of NAT ] means  ex m being Element of NAT st
for F being Function of NAT,ExtREAL st F is V93() holds
(Ser (On (F * H))) . $1 <= (Ser F) . m;
assume A2: H is one-to-one ; ::_thesis: SUM (On (G * H)) <= SUM G
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
given m0 being Element of NAT  such that A4: for F being Function of NAT,ExtREAL st F is V93() holds
(Ser (On (F * H))) . k <= (Ser F) . m0 ; ::_thesis: S1[k + 1]
percases ( k + 1 in S or not k + 1 in S ) ;
supposeA5: k + 1 in S ; ::_thesis: S1[k + 1]
reconsider m1 = H . (k + 1) as Element of NAT ;
set m = m0 + m1;
take  m0 + m1 ; ::_thesis: for F being Function of NAT,ExtREAL st F is V93() holds
(Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1)
let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies (Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1) )
defpred S2[ Element of NAT , Element of ExtREAL ] means ( ( $1 = H . (k + 1) implies $2 = F . $1 ) & ( $1 <> H . (k + 1) implies $2 = 0. ) );
A6: for n being Element of NAT ex y being Element of ExtREAL st S2[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of ExtREAL st S2[n,y]
percases ( n = H . (k + 1) or n <> H . (k + 1) ) ;
supposeA7: n = H . (k + 1) ; ::_thesis: ex y being Element of ExtREAL st S2[n,y]
take  F . n ; ::_thesis: S2[n,F . n]
thus  S2[n,F . n] by A7; ::_thesis: verum
end;
supposeA8: n <> H . (k + 1) ; ::_thesis: ex y being Element of ExtREAL st S2[n,y]
take  0. ; ::_thesis: S2[n, 0. ]
thus  S2[n, 0. ] by A8; ::_thesis: verum
end;
end;
end;
consider G0 being Function of NAT,ExtREAL such that
A9: for n being Element of NAT holds S2[n,G0 . n] from FUNCT_2:sch_3(A6);
reconsider GG0 = On (G0 * H) as Function of NAT,ExtREAL ;
A10: for n being Element of NAT st n <> k + 1 holds
GG0 . n = 0.
proof
let n be Element of NAT ; ::_thesis: ( n <> k + 1 implies GG0 . n = 0. )
assume A11: n <> k + 1 ; ::_thesis: GG0 . n = 0.
percases ( n in S or not n in S ) ;
supposeA12: n in S ; ::_thesis: GG0 . n = 0.
then A13: GG0 . n = (G0 * H) . n by Def1
.= G0 . (H . n) by A12, FUNCT_2:15 ;
reconsider n = n as Element of S by A12;
 not H . n = H . (k + 1) by A2, A5, A11, FUNCT_2:19;
hence  GG0 . n = 0. by A9, A13; ::_thesis: verum
end;
suppose not n in S ; ::_thesis: GG0 . n = 0.
hence  GG0 . n = 0. by Def1; ::_thesis: verum
end;
end;
end;
assume A14: F is V93() ; ::_thesis: (Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1)
 for n being Element of NAT holds 0. <= G0 . n
proof
let n be Element of NAT ; ::_thesis: 0. <= G0 . n
percases ( n = H . (k + 1) or not n = H . (k + 1) ) ;
suppose n = H . (k + 1) ; ::_thesis: 0. <= G0 . n
then  G0 . n = F . n by A9;
hence  0. <= G0 . n by A14, SUPINF_2:39; ::_thesis: verum
end;
suppose not n = H . (k + 1) ; ::_thesis: 0. <= G0 . n
hence  0. <= G0 . n by A9; ::_thesis: verum
end;
end;
end;
then A15: G0 is V93() by SUPINF_2:39;
reconsider n = k + 1 as Element of S by A5;
defpred S3[ Element of NAT , Element of ExtREAL ] means ( ( $1 <> H . (k + 1) implies $2 = F . $1 ) & ( $1 = H . (k + 1) implies $2 = 0. ) );
A16: for n being Element of NAT ex y being Element of ExtREAL st S3[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of ExtREAL st S3[n,y]
percases ( n <> H . (k + 1) or n = H . (k + 1) ) ;
supposeA17: n <> H . (k + 1) ; ::_thesis: ex y being Element of ExtREAL st S3[n,y]
take  F . n ; ::_thesis: S3[n,F . n]
thus  S3[n,F . n] by A17; ::_thesis: verum
end;
supposeA18: n = H . (k + 1) ; ::_thesis: ex y being Element of ExtREAL st S3[n,y]
take  0. ; ::_thesis: S3[n, 0. ]
thus  S3[n, 0. ] by A18; ::_thesis: verum
end;
end;
end;
consider G1 being Function of NAT,ExtREAL such that
A19: for n being Element of NAT holds S3[n,G1 . n] from FUNCT_2:sch_3(A16);
set GG1 = On (G1 * H);
A20: (On (G1 * H)) . (k + 1) = (G1 * H) . n by Def1
.= G1 . (H . n) by FUNCT_2:15
.= 0. by A19 ;
A21: GG0 . n = (G0 * H) . n by Def1
.= G0 . (H . n) by FUNCT_2:15
.= F . (H . n) by A9 ;
then A22: (Ser GG0) . (k + 1) = F . (H . (k + 1)) by A10, Th9;
A23: for n being Element of NAT st n <> k + 1 & n in S holds
(On (G1 * H)) . n = F . (H . n)
proof
let n be Element of NAT ; ::_thesis: ( n <> k + 1 & n in S implies (On (G1 * H)) . n = F . (H . n) )
assume that
A24: n <> k + 1 and
A25: n in S ; ::_thesis: (On (G1 * H)) . n = F . (H . n)
A26: (On (G1 * H)) . n = (G1 * H) . n by A25, Def1
.= G1 . (H . n) by A25, FUNCT_2:15 ;
reconsider n = n as Element of S by A25;
 not H . n = H . (k + 1) by A2, A5, A24, FUNCT_2:19;
hence  (On (G1 * H)) . n = F . (H . n) by A19, A26; ::_thesis: verum
end;
A27: for n being Element of NAT holds (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
proof
let n be Element of NAT ; ::_thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
percases ( n = k + 1 or n <> k + 1 ) ;
supposeA28: n = k + 1 ; ::_thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
then (On (F * H)) . n = (F * H) . n by A5, Def1
.= F . (H . n) by A5, A28, FUNCT_2:15
.= (GG0 . n) + ((On (G1 * H)) . n) by A21, A20, A28, XXREAL_3:4 ;
hence  (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; ::_thesis: verum
end;
supposeA29: n <> k + 1 ; ::_thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
now__::_thesis:_(On_(F_*_H))_._n_=_(GG0_._n)_+_((On_(G1_*_H))_._n)
percases ( n in S or not n in S ) ;
supposeA30: n in S ; ::_thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
then A31: (On (G1 * H)) . n = F . (H . n) by A23, A29;
A32: GG0 . n = 0. by A10, A29;
(On (F * H)) . n = (F * H) . n by A30, Def1
.= F . (H . n) by A30, FUNCT_2:15
.= (GG0 . n) + ((On (G1 * H)) . n) by A32, A31, XXREAL_3:4 ;
hence  (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; ::_thesis: verum
end;
supposeA33: not n in S ; ::_thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
then A34: (On (G1 * H)) . n = 0. by Def1;
A35: GG0 . n = 0. by A10, A29;
(On (F * H)) . n = 0. by A33, Def1
.= (GG0 . n) + ((On (G1 * H)) . n) by A35, A34, XXREAL_3:4 ;
hence  (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; ::_thesis: verum
end;
end;
end;
hence  (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; ::_thesis: verum
end;
end;
end;
 m1 <= m0 + m1 by NAT_1:11;
then A36: (Ser G0) . (m0 + m1) = G0 . (H . (k + 1)) by A9, Th9;
set v = H . n;
A37: (Ser (On (G1 * H))) . (k + 1) = ((Ser (On (G1 * H))) . k) + ((On (G1 * H)) . (k + 1)) by SUPINF_2:44
.= (Ser (On (G1 * H))) . k by A20, XXREAL_3:4 ;
A38: G0 . (H . n) = F . (H . n) by A9;
 for n being Element of NAT holds 0. <= G1 . n
proof
let n be Element of NAT ; ::_thesis: 0. <= G1 . n
percases ( n <> H . (k + 1) or n = H . (k + 1) ) ;
suppose n <> H . (k + 1) ; ::_thesis: 0. <= G1 . n
then  G1 . n = F . n by A19;
hence  0. <= G1 . n by A14, SUPINF_2:39; ::_thesis: verum
end;
suppose n = H . (k + 1) ; ::_thesis: 0. <= G1 . n
hence  0. <= G1 . n by A19; ::_thesis: verum
end;
end;
end;
then A39: G1 is V93() by SUPINF_2:39;
then  G1 * H is V93() by MEASURE1:25;
then A40: On (G1 * H) is V93() by Th7;
 G0 * H is V93() by A15, MEASURE1:25;
then  GG0 is V93() by Th7;
then A41: (Ser (On (F * H))) . (k + 1) = ((Ser GG0) . (k + 1)) + ((Ser (On (G1 * H))) . (k + 1)) by A40, A27, Th3;
 ( (Ser (On (G1 * H))) . k <= (Ser G1) . m0 & (Ser G1) . m0 <= (Ser G1) . (m0 + m1) ) by A4, A39, Th8, NAT_1:11;
then A42: (Ser (On (G1 * H))) . (k + 1) <= (Ser G1) . (m0 + m1) by A37, XXREAL_0:2;
 for m being Element of NAT holds F . m = (G0 . m) + (G1 . m)
proof
let m be Element of NAT ; ::_thesis: F . m = (G0 . m) + (G1 . m)
percases ( m = H . (k + 1) or m <> H . (k + 1) ) ;
suppose m = H . (k + 1) ; ::_thesis: F . m = (G0 . m) + (G1 . m)
then  ( G0 . m = F . m & G1 . m = 0. ) by A9, A19;
hence  F . m = (G0 . m) + (G1 . m) by XXREAL_3:4; ::_thesis: verum
end;
suppose m <> H . (k + 1) ; ::_thesis: F . m = (G0 . m) + (G1 . m)
then  ( G0 . m = 0. & G1 . m = F . m ) by A9, A19;
hence  F . m = (G0 . m) + (G1 . m) by XXREAL_3:4; ::_thesis: verum
end;
end;
end;
then  (Ser F) . (m0 + m1) = ((Ser G0) . (m0 + m1)) + ((Ser G1) . (m0 + m1)) by A15, A39, Th3;
hence  (Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1) by A22, A36, A38, A42, A41, XXREAL_3:36; ::_thesis: verum
end;
supposeA43: not k + 1 in S ; ::_thesis: S1[k + 1]
take  m0 ; ::_thesis: for F being Function of NAT,ExtREAL st F is V93() holds
(Ser (On (F * H))) . (k + 1) <= (Ser F) . m0
let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies (Ser (On (F * H))) . (k + 1) <= (Ser F) . m0 )
A44: (On (F * H)) . (k + 1) = 0. by A43, Def1;
assume A45: F is V93() ; ::_thesis: (Ser (On (F * H))) . (k + 1) <= (Ser F) . m0
(Ser (On (F * H))) . (k + 1) = ((Ser (On (F * H))) . k) + ((On (F * H)) . (k + 1)) by SUPINF_2:44
.= (Ser (On (F * H))) . k by A44, XXREAL_3:4 ;
hence  (Ser (On (F * H))) . (k + 1) <= (Ser F) . m0 by A4, A45; ::_thesis: verum
end;
end;
end;
A46: S1[ 0 ]
proof
percases ( 0 in S or not 0 in S ) ;
supposeA47: 0 in S ; ::_thesis: S1[ 0 ]
reconsider m = H . 0 as Element of NAT ;
take  m ; ::_thesis: for F being Function of NAT,ExtREAL st F is V93() holds
(Ser (On (F * H))) . 0 <= (Ser F) . m
let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies (Ser (On (F * H))) . 0 <= (Ser F) . m )
 (Ser (On (F * H))) . 0 = (On (F * H)) . 0 by SUPINF_2:44;
then A48: (Ser (On (F * H))) . 0 = (F * H) . 0 by A47, Def1
.= F . (H . 0) by A47, FUNCT_2:15 ;
assume  F is V93() ; ::_thesis: (Ser (On (F * H))) . 0 <= (Ser F) . m
hence  (Ser (On (F * H))) . 0 <= (Ser F) . m by A48, Th2; ::_thesis: verum
end;
supposeA49: not 0 in S ; ::_thesis: S1[ 0 ]
take m = 0 ; ::_thesis: for F being Function of NAT,ExtREAL st F is V93() holds
(Ser (On (F * H))) . 0 <= (Ser F) . m
let F be Function of NAT,ExtREAL; ::_thesis: ( F is V93() implies (Ser (On (F * H))) . 0 <= (Ser F) . m )
assume  F is V93() ; ::_thesis: (Ser (On (F * H))) . 0 <= (Ser F) . m
then A50: ( 0. <= F . 0 & F . 0 <= (Ser F) . m ) by Th2, SUPINF_2:39;
 (Ser (On (F * H))) . 0 = (On (F * H)) . 0 by SUPINF_2:44;
then  (Ser (On (F * H))) . 0 = 0. by A49, Def1;
hence  (Ser (On (F * H))) . 0 <= (Ser F) . m by A50, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A51: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A46, A3);
 for x being ext-real number st x in rng (Ser (On (G * H))) holds
ex y being ext-real number st
( y in rng (Ser G) & x <= y )
proof
let x be ext-real number ; ::_thesis: ( x in rng (Ser (On (G * H))) implies ex y being ext-real number st
( y in rng (Ser G) & x <= y ) )
assume A52: x in rng (Ser (On (G * H))) ; ::_thesis: ex y being ext-real number st
( y in rng (Ser G) & x <= y )
 ex y being ext-real number st
( y in rng (Ser G) & x <= y )
proof
consider n being set  such that
A53: n in dom (Ser (On (G * H))) and
A54: x = (Ser (On (G * H))) . n by A52, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A53;
consider m being Element of NAT  such that
A55: for F being Function of NAT,ExtREAL st F is V93() holds
(Ser (On (F * H))) . n <= (Ser F) . m by A51;
take  (Ser G) . m ; ::_thesis: ( (Ser G) . m in rng (Ser G) & x <= (Ser G) . m )
 dom (Ser G) = NAT by FUNCT_2:def_1;
hence  ( (Ser G) . m in rng (Ser G) & x <= (Ser G) . m ) by A1, A54, A55, FUNCT_1:def_3; ::_thesis: verum
end;
hence  ex y being ext-real number st
( y in rng (Ser G) & x <= y ) ; ::_thesis: verum
end;
then A56: sup (rng (Ser (On (G * H)))) <= sup (rng (Ser G)) by XXREAL_2:63;
 SUM G = sup (rng (Ser G)) by SUPINF_2:def_17;
hence  SUM (On (G * H)) <= SUM G by A56, SUPINF_2:def_17; ::_thesis: verum
end;

theorem Th11: :: MEASURE7:11
for F, G being Function of NAT,ExtREAL st G is V93() holds
for S being non empty Subset of NAT
for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds
( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds
SUM F <= SUM G
proof
let F, G be Function of NAT,ExtREAL; ::_thesis: ( G is V93() implies for S being non empty Subset of NAT
for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds
( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds
SUM F <= SUM G )
assume A1: G is V93() ; ::_thesis: for S being non empty Subset of NAT
for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds
( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds
SUM F <= SUM G
let S be non empty Subset of NAT; ::_thesis: for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds
( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds
SUM F <= SUM G
let H be Function of S,NAT; ::_thesis: ( H is one-to-one & ( for k being Element of NAT holds
( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) implies SUM F <= SUM G )
assume A2: H is one-to-one ; ::_thesis: ( ex k being Element of NAT st
( ( k in S implies F . k = (G * H) . k ) implies ( not k in S & not F . k = 0. ) ) or SUM F <= SUM G )
assume  for k being Element of NAT holds
( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ; ::_thesis: SUM F <= SUM G
then  F = On (G * H) by Def1;
hence  SUM F <= SUM G by A1, A2, Th10; ::_thesis: verum
end;

 REAL in bool REAL
by ZFMISC_1:def_1;

then reconsider G0 = NAT --> REAL as Function of NAT,(bool REAL) by FUNCOP_1:45;

Lm1:  rng G0 = {REAL}
by FUNCOP_1:8;

then Lm2:  REAL c= union (rng G0)
by ZFMISC_1:25;

Lm3:  for n being Element of NAT holds G0 . n is Interval
proof
let n be Element of NAT ; ::_thesis: G0 . n is Interval
 G0 . n in {REAL} by Lm1, FUNCT_2:4;
hence  G0 . n is Interval by TARSKI:def_1; ::_thesis: verum
end;

definition
let A be Subset of REAL;
mode Interval_Covering of A ->  Function of NAT,(bool REAL) means :Def2: :: MEASURE7:def 2
( A c= union (rng it) & ( for n being Element of NAT holds it . n is Interval ) );
existence
 ex b1 being Function of NAT,(bool REAL) st
( A c= union (rng b1) & ( for n being Element of NAT holds b1 . n is Interval ) ) by Lm2, Lm3, XBOOLE_1:1;
end;

:: deftheorem Def2 defines Interval_Covering MEASURE7:def_2_:_
 for A being Subset of REAL
for b2 being Function of NAT,(bool REAL) holds
( b2 is Interval_Covering of A iff ( A c= union (rng b2) & ( for n being Element of NAT holds b2 . n is Interval ) ) );

definition
let A be Subset of REAL;
let F be Interval_Covering of A;
let n be Element of NAT ;
:: original: .
redefine funcF . n ->  Interval;
correctness
coherence
F . n is Interval;
by Def2;
end;

definition
let F be Function of NAT,(bool REAL);
mode Interval_Covering of F ->  Function of NAT,(Funcs (NAT,(bool REAL))) means :Def3: :: MEASURE7:def 3
 for n being Element of NAT holds it . n is Interval_Covering of F . n;
existence
 ex b1 being Function of NAT,(Funcs (NAT,(bool REAL))) st
for n being Element of NAT holds b1 . n is Interval_Covering of F . n
proof
reconsider G = G0 as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8;
reconsider H = NAT --> G as Function of NAT,(Funcs (NAT,(bool REAL))) ;
take  H ; ::_thesis: for n being Element of NAT holds H . n is Interval_Covering of F . n
A1: for n being Element of NAT holds G0 is Interval_Covering of F . n
proof
let n be Element of NAT ; ::_thesis: G0 is Interval_Covering of F . n
 F . n c= union (rng G0) by Lm2, XBOOLE_1:1;
hence  G0 is Interval_Covering of F . n by Def2, Lm3; ::_thesis: verum
end;
 for n being Element of NAT holds H . n is Interval_Covering of F . n
proof
let n be Element of NAT ; ::_thesis: H . n is Interval_Covering of F . n
 H . n = G by FUNCOP_1:7;
hence  H . n is Interval_Covering of F . n by A1; ::_thesis: verum
end;
hence  for n being Element of NAT holds H . n is Interval_Covering of F . n ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Interval_Covering MEASURE7:def_3_:_
 for F being Function of NAT,(bool REAL)
for b2 being Function of NAT,(Funcs (NAT,(bool REAL))) holds
( b2 is Interval_Covering of F iff for n being Element of NAT holds b2 . n is Interval_Covering of F . n );

definition
let A be Subset of REAL;
let F be Interval_Covering of A;
deffunc H1( Element of NAT ) ->  Element of ExtREAL = diameter (F . $1);
funcF vol  ->  Function of NAT,ExtREAL means :Def4: :: MEASURE7:def 4
 for n being Element of NAT holds it . n = diameter (F . n);
existence
 ex b1 being Function of NAT,ExtREAL st
for n being Element of NAT holds b1 . n = diameter (F . n)
proof
thus  ex G being Function of NAT,ExtREAL st
for n being Element of NAT holds G . n = H1(n) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds b1 . n = diameter (F . n) ) & ( for n being Element of NAT holds b2 . n = diameter (F . n) ) holds
b1 = b2
proof
thus  for G1, G2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds G1 . n = H1(n) ) & ( for n being Element of NAT holds G2 . n = H1(n) ) holds
G1 = G2 from BINOP_2:sch_1(); ::_thesis: verum
end;
end;

:: deftheorem Def4 defines vol MEASURE7:def_4_:_
 for A being Subset of REAL
for F being Interval_Covering of A
for b3 being Function of NAT,ExtREAL holds
( b3 = F vol iff for n being Element of NAT holds b3 . n = diameter (F . n) );

theorem Th12: :: MEASURE7:12
for A being Subset of REAL
for F being Interval_Covering of A holds F vol is V93()
proof
let A be Subset of REAL; ::_thesis: for F being Interval_Covering of A holds F vol is V93()
let F be Interval_Covering of A; ::_thesis: F vol is V93()
 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 V93() by SUPINF_2:39; ::_thesis: verum
end;

definition
let F be Function of NAT,(bool REAL);
let H be Interval_Covering of F;
let n be Element of NAT ;
:: original: .
redefine funcH . n ->  Interval_Covering of F . n;
correctness
coherence
H . n is Interval_Covering of F . n;
by Def3;
end;

definition
let F be Function of NAT,(bool REAL);
let G be Interval_Covering of F;
funcG vol  ->  Function of NAT,(Funcs (NAT,ExtREAL)) means :: MEASURE7:def 5
 for n being Element of NAT holds it . n = (G . n) vol ;
existence
 ex b1 being Function of NAT,(Funcs (NAT,ExtREAL)) st
for n being Element of NAT holds b1 . n = (G . n) vol
proof
defpred S1[ Element of NAT , set ] means $2 = (G . $1) vol ;
A1: for n being Element of NAT ex y being Element of Funcs (NAT,ExtREAL) st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of Funcs (NAT,ExtREAL) st S1[n,y]
 (G . n) vol is Element of Funcs (NAT,ExtREAL) by FUNCT_2:8;
hence  ex y being Element of Funcs (NAT,ExtREAL) st S1[n,y] ; ::_thesis: verum
end;
 ex G0 being Function of NAT,(Funcs (NAT,ExtREAL)) st
for n being Element of NAT holds S1[n,G0 . n] from FUNCT_2:sch_3(A1);
hence  ex b1 being Function of NAT,(Funcs (NAT,ExtREAL)) st
for n being Element of NAT holds b1 . n = (G . n) vol ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of NAT,(Funcs (NAT,ExtREAL)) st ( for n being Element of NAT holds b1 . n = (G . n) vol ) & ( for n being Element of NAT holds b2 . n = (G . n) vol ) holds
b1 = b2
proof
deffunc H1( Element of NAT ) ->  Function of NAT,ExtREAL = (G . $1) vol ;
thus  for F1, F2 being Function of NAT,(Funcs (NAT,ExtREAL)) st ( for n being Element of NAT holds F1 . n = H1(n) ) & ( for n being Element of NAT holds F2 . n = H1(n) ) holds
F1 = F2 from BINOP_2:sch_1(); ::_thesis: verum
end;
end;

:: deftheorem  defines vol MEASURE7:def_5_:_
 for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F
for b3 being Function of NAT,(Funcs (NAT,ExtREAL)) holds
( b3 = G vol iff for n being Element of NAT holds b3 . n = (G . n) vol );

definition
let A be Subset of REAL;
let F be Interval_Covering of A;
func vol F ->  R_eal equals :: MEASURE7:def 6
 SUM (F vol);
correctness
coherence
SUM (F vol) is R_eal;
;
end;

:: deftheorem  defines vol MEASURE7:def_6_:_
 for A being Subset of REAL
for F being Interval_Covering of A holds vol F = SUM (F vol);

definition
let F be Function of NAT,(bool REAL);
let G be Interval_Covering of F;
func vol G ->  Function of NAT,ExtREAL means :Def7: :: MEASURE7:def 7
 for n being Element of NAT holds it . n = vol (G . n);
existence
 ex b1 being Function of NAT,ExtREAL st
for n being Element of NAT holds b1 . n = vol (G . n)
proof
defpred S1[ Element of NAT , Element of ExtREAL ] means $2 = vol (G . $1);
A1: for n being Element of NAT ex y being Element of ExtREAL st S1[n,y] ;
consider G0 being Function of NAT,ExtREAL such that
A2: for n being Element of NAT holds S1[n,G0 . n] from FUNCT_2:sch_3(A1);
take  G0 ; ::_thesis: for n being Element of NAT holds G0 . n = vol (G . n)
thus  for n being Element of NAT holds G0 . n = vol (G . n) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds b1 . n = vol (G . n) ) & ( for n being Element of NAT holds b2 . n = vol (G . n) ) holds
b1 = b2
proof
deffunc H1( Element of NAT ) ->  R_eal = vol (G . $1);
thus  for F1, F2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds F1 . n = H1(n) ) & ( for n being Element of NAT holds F2 . n = H1(n) ) holds
F1 = F2 from BINOP_2:sch_1(); ::_thesis: verum
end;
end;

:: deftheorem Def7 defines vol MEASURE7:def_7_:_
 for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F
for b3 being Function of NAT,ExtREAL holds
( b3 = vol G iff for n being Element of NAT holds b3 . n = vol (G . n) );

theorem Th13: :: MEASURE7:13
for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F
for n being Element of NAT holds 0. <= (vol G) . n
proof
let F be Function of NAT,(bool REAL); ::_thesis: for G being Interval_Covering of F
for n being Element of NAT holds 0. <= (vol G) . n
let G be Interval_Covering of F; ::_thesis: for n being Element of NAT holds 0. <= (vol G) . n
let n be Element of NAT ; ::_thesis: 0. <= (vol G) . n
 for k being Element of NAT holds 0. <= ((G . n) vol) . k
proof
let k be Element of NAT ; ::_thesis: 0. <= ((G . n) vol) . k
 0. <= diameter ((G . n) . k) by MEASURE5:13;
hence  0. <= ((G . n) vol) . k by Def4; ::_thesis: verum
end;
then A1: (G . n) vol is V93() by SUPINF_2:39;
 (vol G) . n = vol (G . n) by Def7;
hence  0. <= (vol G) . n by A1, MEASURE6:2; ::_thesis: verum
end;

definition
let A be Subset of REAL;
defpred S1[ set ] means  ex F being Interval_Covering of A st $1 = vol F;
func Svc A ->  Subset of ExtREAL means :Def8: :: MEASURE7:def 8
 for x being R_eal holds
( x in it iff ex F being Interval_Covering of A st x = vol F );
existence
 ex b1 being Subset of ExtREAL st
for x being R_eal holds
( x in b1 iff ex F being Interval_Covering of A st x = vol F )
proof
consider D being set  such that
A1: for x being set holds
( x in D iff ( x in ExtREAL & S1[x] ) ) from XBOOLE_0:sch_1();
 for z being set st z in D holds
z in ExtREAL by A1;
then reconsider D = D as Subset of ExtREAL by TARSKI:def_3;
take  D ; ::_thesis: for x being R_eal holds
( x in D iff ex F being Interval_Covering of A st x = vol F )
thus  for x being R_eal holds
( x in D iff ex F being Interval_Covering of A st x = vol F ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of ExtREAL st ( for x being R_eal holds
( x in b1 iff ex F being Interval_Covering of A st x = vol F ) ) & ( for x being R_eal holds
( x in b2 iff ex F being Interval_Covering of A st x = vol F ) ) holds
b1 = b2
proof
let D1, D2 be Subset of ExtREAL; ::_thesis: ( ( for x being R_eal holds
( x in D1 iff ex F being Interval_Covering of A st x = vol F ) ) & ( for x being R_eal holds
( x in D2 iff ex F being Interval_Covering of A st x = vol F ) ) implies D1 = D2 )
assume that
A2: for x being R_eal holds
( x in D1 iff S1[x] ) and
A3: for x being R_eal holds
( x in D2 iff S1[x] ) ; ::_thesis: D1 = D2
thus  D1 = D2 from SUBSET_1:sch_2(A2, A3); ::_thesis: verum
end;
end;

:: deftheorem Def8 defines Svc MEASURE7:def_8_:_
 for A being Subset of REAL
for b2 being Subset of ExtREAL holds
( b2 = Svc A iff for x being R_eal holds
( x in b2 iff ex F being Interval_Covering of A st x = vol F ) );

registration
let A be Subset of REAL;
cluster Svc A ->  non empty ;
coherence
 not Svc A is empty
proof
 REAL c= REAL ;
then consider F0 being Function of NAT,(bool REAL) such that
A1: rng F0 = {REAL,({} REAL)} and
A2: ( F0 . 0 = REAL & ( for n being Element of NAT st 0 < n holds
F0 . n = {} REAL ) ) by MEASURE1:19;
 ( union {REAL,{}} = REAL \/ {} & ( for n being Element of NAT holds F0 . n is Interval ) ) by A2, NAT_1:3, ZFMISC_1:75;
then reconsider F0 = F0 as Interval_Covering of A by A1, Def2;
defpred S1[ set ] means  ex F being Interval_Covering of A st A = vol F;
consider D being set  such that
A3: for x being set holds
( x in D iff ( x in ExtREAL & S1[x] ) ) from XBOOLE_0:sch_1();
 vol F0 in D by A3;
hence  not Svc A is empty by Def8; ::_thesis: verum
end;
end;

definition
let A be Subset of REAL;
func COMPLEX A ->  Element of ExtREAL  equals :: MEASURE7:def 9
 inf (Svc A);
correctness
coherence
inf (Svc A) is Element of ExtREAL ;
;
end;

:: deftheorem  defines COMPLEX MEASURE7:def_9_:_
 for A being Subset of REAL holds COMPLEX A = inf (Svc A);

definition
func OS_Meas  ->  Function of (bool REAL),ExtREAL means :Def10: :: MEASURE7:def 10
 for A being Subset of REAL holds it . A = inf (Svc A);
existence
 ex b1 being Function of (bool REAL),ExtREAL st
for A being Subset of REAL holds b1 . A = inf (Svc A)
proof
consider G being Function of (bool REAL),ExtREAL such that
A1: for A being Subset of REAL holds G . A = COMPLEX A from FUNCT_2:sch_4();
take  G ; ::_thesis: for A being Subset of REAL holds G . A = inf (Svc A)
 for A being Subset of REAL holds G . A = inf (Svc A)
proof
let A be Subset of REAL; ::_thesis: G . A = inf (Svc A)
 G . A = COMPLEX A by A1;
hence  G . A = inf (Svc A) ; ::_thesis: verum
end;
hence  for A being Subset of REAL holds G . A = inf (Svc A) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (bool REAL),ExtREAL st ( for A being Subset of REAL holds b1 . A = inf (Svc A) ) & ( for A being Subset of REAL holds b2 . A = inf (Svc A) ) holds
b1 = b2
proof
deffunc H1( Subset of REAL) ->  Element of ExtREAL = inf (Svc $1);
thus  for F1, F2 being Function of (bool REAL),ExtREAL st ( for A being Subset of REAL holds F1 . A = H1(A) ) & ( for A being Subset of REAL holds F2 . A = H1(A) ) holds
F1 = F2 from BINOP_2:sch_1(); ::_thesis: verum
end;
end;

:: deftheorem Def10 defines OS_Meas MEASURE7:def_10_:_
 for b1 being Function of (bool REAL),ExtREAL holds
( b1 = OS_Meas iff for A being Subset of REAL holds b1 . A = inf (Svc A) );

definition
let F be Function of NAT,(bool REAL);
let G be Interval_Covering of F;
let H be Function of NAT,[:NAT,NAT:];
assume B1: rng H = [:NAT,NAT:] ;
func On (G,H) ->  Interval_Covering of union (rng F) means :Def11: :: MEASURE7:def 11
 for n being Element of NAT holds it . n = (G . ((pr1 H) . n)) . ((pr2 H) . n);
existence
 ex b1 being Interval_Covering of union (rng F) st
for n being Element of NAT holds b1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n)
proof
defpred S1[ Element of NAT , Subset of REAL] means $2 = (G . ((pr1 H) . $1)) . ((pr2 H) . $1);
A1: for n being Element of NAT ex y being Subset of REAL st S1[n,y] ;
consider GG being Function of NAT,(bool REAL) such that
A2: for n being Element of NAT holds S1[n,GG . n] from FUNCT_2:sch_3(A1);
A3: union (rng F) c= union (rng GG)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng F) or x in union (rng GG) )
assume  x in union (rng F) ; ::_thesis: x in union (rng GG)
then consider A being set  such that
A4: x in A and
A5: A in rng F by TARSKI:def_4;
consider n1 being set  such that
A6: n1 in dom F and
A7: A = F . n1 by A5, FUNCT_1:def_3;
reconsider n1 = n1 as Element of NAT by A6;
 F . n1 c= union (rng (G . n1)) by Def2;
then consider AA being set  such that
A8: x in AA and
A9: AA in rng (G . n1) by A4, A7, TARSKI:def_4;
consider n2 being set  such that
A10: n2 in dom (G . n1) and
A11: AA = (G . n1) . n2 by A9, FUNCT_1:def_3;
reconsider n2 = n2 as Element of NAT by A10;
consider n being set  such that
A12: n in dom H and
A13: [n1,n2] = H . n by B1, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A12;
 [((pr1 H) . n),((pr2 H) . n)] = [n1,n2] by A13, FUNCT_2:119;
then  ( (pr1 H) . n = n1 & (pr2 H) . n = n2 ) by XTUPLE_0:1;
then A14: x in GG . n by A2, A8, A11;
 GG . n in rng GG by FUNCT_2:4;
hence  x in union (rng GG) by A14, TARSKI:def_4; ::_thesis: verum
end;
 for n being Element of NAT holds GG . n is Interval
proof
let n be Element of NAT ; ::_thesis: GG . n is Interval
 GG . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) by A2;
hence  GG . n is Interval ; ::_thesis: verum
end;
then reconsider GG = GG as Interval_Covering of union (rng F) by A3, Def2;
take  GG ; ::_thesis: for n being Element of NAT holds GG . n = (G . ((pr1 H) . n)) . ((pr2 H) . n)
thus  for n being Element of NAT holds GG . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Interval_Covering of union (rng F) st ( for n being Element of NAT holds b1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) & ( for n being Element of NAT holds b2 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) holds
b1 = b2
proof
let G1, G2 be Interval_Covering of union (rng F); ::_thesis: ( ( for n being Element of NAT holds G1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) & ( for n being Element of NAT holds G2 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) implies G1 = G2 )
assume that
A15: for n being Element of NAT holds G1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) and
A16: for n being Element of NAT holds G2 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ; ::_thesis: G1 = G2
 for n being set st n in NAT holds
G1 . n = G2 . n
proof
let n be set ; ::_thesis: ( n in NAT implies G1 . n = G2 . n )
assume  n in NAT ; ::_thesis: G1 . n = G2 . n
then reconsider n = n as Element of NAT ;
 G1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) by A15;
hence  G1 . n = G2 . n by A16; ::_thesis: verum
end;
hence  G1 = G2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines On MEASURE7:def_11_:_
 for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F
for H being Function of NAT,[:NAT,NAT:] st rng H = [:NAT,NAT:] holds
for b4 being Interval_Covering of union (rng F) holds
( b4 = On (G,H) iff for n being Element of NAT holds b4 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) );

reconsider D = NAT --> ({} REAL) as Function of NAT,(bool REAL) ;

theorem Th14: :: MEASURE7:14
for H being Function of NAT,[:NAT,NAT:] st H is one-to-one & rng H = [:NAT,NAT:] holds
for k being Element of NAT ex m being Element of NAT st
for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m
proof
reconsider y = D as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8;
let H be Function of NAT,[:NAT,NAT:]; ::_thesis: ( H is one-to-one & rng H = [:NAT,NAT:] implies for k being Element of NAT ex m being Element of NAT st
for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m )
assume that
A1: H is one-to-one and
A2: rng H = [:NAT,NAT:] ; ::_thesis: for k being Element of NAT ex m being Element of NAT st
for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m
defpred S1[ Element of NAT ] means  ex m being Element of NAT st
for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . $1 <= (Ser (vol G)) . m;
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
set N0 =  {  s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s  }  ;
A4:  {  s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s  }  c= NAT
proof
let s1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not s1 in  {  s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s  }  or s1 in NAT )
assume  s1 in  {  s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s  }  ; ::_thesis: s1 in NAT
then  ex s being Element of NAT st
( s = s1 & (pr1 H) . (k + 1) = (pr1 H) . s ) ;
hence  s1 in NAT ; ::_thesis: verum
end;
 k + 1 in  {  s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s  }  ;
then reconsider N0 =  {  s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s  }  as non empty Subset of NAT by A4;
given m0 being Element of NAT  such that A5: for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m0 ; ::_thesis: S1[k + 1]
take m = m0 + ((pr1 H) . (k + 1)); ::_thesis: for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m
let F be Function of NAT,(bool REAL); ::_thesis: for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m
let G be Interval_Covering of F; ::_thesis: (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m
defpred S2[ Element of NAT , Function] means ( ( $1 <> (pr1 H) . (k + 1) implies for m being Element of NAT holds $2 . m = (G . $1) . m ) & ( $1 = (pr1 H) . (k + 1) implies for m being Element of NAT holds $2 . m = {} ) );
A6: for n being Element of NAT ex y being Element of Funcs (NAT,(bool REAL)) st S2[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S2[n,y]
percases ( n <> (pr1 H) . (k + 1) or n = (pr1 H) . (k + 1) ) ;
supposeA7: n <> (pr1 H) . (k + 1) ; ::_thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S2[n,y]
reconsider y = G . n as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8;
take  y ; ::_thesis: S2[n,y]
thus  S2[n,y] by A7; ::_thesis: verum
end;
supposeA8: n = (pr1 H) . (k + 1) ; ::_thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S2[n,y]
take  y ; ::_thesis: S2[n,y]
thus  S2[n,y] by A8, FUNCOP_1:7; ::_thesis: verum
end;
end;
end;
consider G1 being Function of NAT,(Funcs (NAT,(bool REAL))) such that
A9: for n being Element of NAT holds S2[n,G1 . n] from FUNCT_2:sch_3(A6);
A10: for n being Element of NAT holds G1 . n is Interval_Covering of D . n
proof
let n be Element of NAT ; ::_thesis: G1 . n is Interval_Covering of D . n
consider f0 being Function such that
A11: G1 . n = f0 and
A12: ( dom f0 = NAT & rng f0 c= bool REAL ) by FUNCT_2:def_2;
reconsider f0 = f0 as Function of NAT,(bool REAL) by A12, FUNCT_2:2;
A13: for s being Element of NAT holds f0 . s is Interval
proof
let s be Element of NAT ; ::_thesis: f0 . s is Interval
percases ( n <> (pr1 H) . (k + 1) or n = (pr1 H) . (k + 1) ) ;
suppose n <> (pr1 H) . (k + 1) ; ::_thesis: f0 . s is Interval
then  f0 . s = (G . n) . s by A9, A11;
hence  f0 . s is Interval ; ::_thesis: verum
end;
suppose n = (pr1 H) . (k + 1) ; ::_thesis: f0 . s is Interval
hence  f0 . s is Interval by A9, A11; ::_thesis: verum
end;
end;
end;
 D . n = {} by FUNCOP_1:7;
then  D . n c= union (rng f0) by XBOOLE_1:2;
then reconsider f0 = f0 as Interval_Covering of D . n by A13, Def2;
 G1 . n = f0 by A11;
hence  G1 . n is Interval_Covering of D . n ; ::_thesis: verum
end;
defpred S3[ Element of N0, Element of NAT ] means $2 = (pr2 H) . $1;
defpred S4[ Element of NAT , Function] means ( ( $1 = (pr1 H) . (k + 1) implies for m being Element of NAT holds $2 . m = (G . $1) . m ) & ( $1 <> (pr1 H) . (k + 1) implies for m being Element of NAT holds $2 . m = {} ) );
A14: for n being Element of NAT ex y being Element of Funcs (NAT,(bool REAL)) st S4[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S4[n,y]
percases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ;
supposeA15: n = (pr1 H) . (k + 1) ; ::_thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S4[n,y]
reconsider y = G . n as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8;
take  y ; ::_thesis: S4[n,y]
thus  S4[n,y] by A15; ::_thesis: verum
end;
supposeA16: n <> (pr1 H) . (k + 1) ; ::_thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S4[n,y]
take  y ; ::_thesis: S4[n,y]
thus  S4[n,y] by A16, FUNCOP_1:7; ::_thesis: verum
end;
end;
end;
consider G0 being Function of NAT,(Funcs (NAT,(bool REAL))) such that
A17: for n being Element of NAT holds S4[n,G0 . n] from FUNCT_2:sch_3(A14);
 for n being Element of NAT holds G0 . n is Interval_Covering of D . n
proof
let n be Element of NAT ; ::_thesis: G0 . n is Interval_Covering of D . n
consider f0 being Function such that
A18: G0 . n = f0 and
A19: ( dom f0 = NAT & rng f0 c= bool REAL ) by FUNCT_2:def_2;
reconsider f0 = f0 as Function of NAT,(bool REAL) by A19, FUNCT_2:2;
A20: for s being Element of NAT holds f0 . s is Interval
proof
let s be Element of NAT ; ::_thesis: f0 . s is Interval
percases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ;
suppose n = (pr1 H) . (k + 1) ; ::_thesis: f0 . s is Interval
then  f0 . s = (G . n) . s by A17, A18;
hence  f0 . s is Interval ; ::_thesis: verum
end;
suppose n <> (pr1 H) . (k + 1) ; ::_thesis: f0 . s is Interval
hence  f0 . s is Interval by A17, A18; ::_thesis: verum
end;
end;
end;
 D . n = {} by FUNCOP_1:7;
then  D . n c= union (rng f0) by XBOOLE_1:2;
then reconsider f0 = f0 as Interval_Covering of D . n by A20, Def2;
 G0 . n = f0 by A18;
hence  G0 . n is Interval_Covering of D . n ; ::_thesis: verum
end;
then reconsider G0 = G0 as Interval_Covering of D by Def3;
set GG0 = On (G0,H);
reconsider G1 = G1 as Interval_Covering of D by A10, Def3;
set GG1 = On (G1,H);
A21: (Ser ((On (G0,H)) vol)) . (k + 1) <= SUM ((On (G0,H)) vol) by Th6, Th12;
(On (G1,H)) . (k + 1) = (G1 . ((pr1 H) . (k + 1))) . ((pr2 H) . (k + 1)) by A2, Def11
.= {} by A9 ;
then A22: ((On (G1,H)) vol) . (k + 1) = 0. by Def4, MEASURE5:10;
 (Ser ((On (G1,H)) vol)) . (k + 1) = ((Ser ((On (G1,H)) vol)) . k) + (((On (G1,H)) vol) . (k + 1)) by SUPINF_2:44;
then A23: (Ser ((On (G1,H)) vol)) . (k + 1) = (Ser ((On (G1,H)) vol)) . k by A22, XXREAL_3:4;
 for s being Element of NAT holds 0. <= (vol G1) . s by Th13;
then  vol G1 is V93() by SUPINF_2:39;
then A24: (Ser (vol G1)) . m0 <= (Ser (vol G1)) . m by SUPINF_2:41;
A25: for n being Element of NAT holds ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
proof
let n be Element of NAT ; ::_thesis: ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
A26: ( ((On (G0,H)) vol) . n = diameter ((On (G0,H)) . n) & ((On (G1,H)) vol) . n = diameter ((On (G1,H)) . n) ) by Def4;
 ((On (G,H)) vol) . n = diameter ((On (G,H)) . n) by Def4;
then A27: ((On (G,H)) vol) . n = diameter ((G . ((pr1 H) . n)) . ((pr2 H) . n)) by A2, Def11;
percases ( (pr1 H) . n = (pr1 H) . (k + 1) or (pr1 H) . n <> (pr1 H) . (k + 1) ) ;
supposeA28: (pr1 H) . n = (pr1 H) . (k + 1) ; ::_thesis: ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
A29: (On (G1,H)) . n = (G1 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def11
.= {} by A9, A28 ;
(On (G0,H)) . n = (G0 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def11
.= (G . ((pr1 H) . n)) . ((pr2 H) . n) by A17, A28 ;
hence  ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n) by A26, A27, A29, MEASURE5:10, XXREAL_3:4; ::_thesis: verum
end;
supposeA30: (pr1 H) . n <> (pr1 H) . (k + 1) ; ::_thesis: ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
A31: (On (G0,H)) . n = (G0 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def11
.= {} by A17, A30 ;
(On (G1,H)) . n = (G1 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def11
.= (G . ((pr1 H) . n)) . ((pr2 H) . n) by A9, A30 ;
hence  ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n) by A26, A27, A31, MEASURE5:10, XXREAL_3:4; ::_thesis: verum
end;
end;
end;
 ( (On (G0,H)) vol is V93() & (On (G1,H)) vol is V93() ) by Th12;
then A32: (Ser ((On (G,H)) vol)) . (k + 1) = ((Ser ((On (G0,H)) vol)) . (k + 1)) + ((Ser ((On (G1,H)) vol)) . (k + 1)) by A25, Th3;
 for s being Element of NAT holds 0. <= (vol G1) . s by Th13;
then A33: vol G1 is V93() by SUPINF_2:39;
 (Ser ((On (G1,H)) vol)) . k <= (Ser (vol G1)) . m0 by A5;
then A34: (Ser ((On (G1,H)) vol)) . (k + 1) <= (Ser (vol G1)) . m by A23, A24, XXREAL_0:2;
A35: for s being Element of N0 ex y being Element of NAT st S3[s,y] ;
consider SOS being Function of N0,NAT such that
A36: for s being Element of N0 holds S3[s,SOS . s] from FUNCT_2:sch_3(A35);
A37: for n being Element of NAT holds (vol G) . n = ((vol G0) . n) + ((vol G1) . n)
proof
let n be Element of NAT ; ::_thesis: (vol G) . n = ((vol G0) . n) + ((vol G1) . n)
A38: vol (G . n) = (vol (G0 . n)) + (vol (G1 . n))
proof
percases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ;
supposeA39: n = (pr1 H) . (k + 1) ; ::_thesis: vol (G . n) = (vol (G0 . n)) + (vol (G1 . n))
 for s being Element of NAT holds ((G . n) vol) . s <= ((G0 . n) vol) . s
proof
let s be Element of NAT ; ::_thesis: ((G . n) vol) . s <= ((G0 . n) vol) . s
((G0 . n) vol) . s = diameter ((G0 . n) . s) by Def4
.= diameter ((G . n) . s) by A17, A39
.= ((G . n) vol) . s by Def4 ;
hence  ((G . n) vol) . s <= ((G0 . n) vol) . s ; ::_thesis: verum
end;
then A40: SUM ((G . n) vol) <= SUM ((G0 . n) vol) by SUPINF_2:43;
 for s being Element of NAT holds ((G1 . n) vol) . s = 0.
proof
let s be Element of NAT ; ::_thesis: ((G1 . n) vol) . s = 0.
 diameter ((G1 . n) . s) = 0. by A9, A39, MEASURE5:10;
hence  ((G1 . n) vol) . s = 0. by Def4; ::_thesis: verum
end;
then A41: SUM ((G1 . n) vol) = 0. by Th1;
 for s being Element of NAT holds ((G0 . n) vol) . s <= ((G . n) vol) . s
proof
let s be Element of NAT ; ::_thesis: ((G0 . n) vol) . s <= ((G . n) vol) . s
((G0 . n) vol) . s = diameter ((G0 . n) . s) by Def4
.= diameter ((G . n) . s) by A17, A39
.= ((G . n) vol) . s by Def4 ;
hence  ((G0 . n) vol) . s <= ((G . n) vol) . s ; ::_thesis: verum
end;
then  SUM ((G0 . n) vol) <= SUM ((G . n) vol) by SUPINF_2:43;
then  SUM ((G . n) vol) = SUM ((G0 . n) vol) by A40, XXREAL_0:1;
hence  vol (G . n) = (vol (G0 . n)) + (vol (G1 . n)) by A41, XXREAL_3:4; ::_thesis: verum
end;
supposeA42: n <> (pr1 H) . (k + 1) ; ::_thesis: vol (G . n) = (vol (G0 . n)) + (vol (G1 . n))
A43: for s being Element of NAT holds ((G1 . n) vol) . s = ((G . n) vol) . s
proof
let s be Element of NAT ; ::_thesis: ((G1 . n) vol) . s = ((G . n) vol) . s
 ( ((G1 . n) vol) . s = diameter ((G1 . n) . s) & ((G . n) vol) . s = diameter ((G . n) . s) ) by Def4;
hence  ((G1 . n) vol) . s = ((G . n) vol) . s by A9, A42; ::_thesis: verum
end;
then  for s being Element of NAT holds ((G . n) vol) . s <= ((G1 . n) vol) . s ;
then A44: SUM ((G . n) vol) <= SUM ((G1 . n) vol) by SUPINF_2:43;
 for s being Element of NAT holds ((G0 . n) vol) . s = 0.
proof
let s be Element of NAT ; ::_thesis: ((G0 . n) vol) . s = 0.
 diameter ((G0 . n) . s) = 0. by A17, A42, MEASURE5:10;
hence  ((G0 . n) vol) . s = 0. by Def4; ::_thesis: verum
end;
then A45: SUM ((G0 . n) vol) = 0. by Th1;
 for s being Element of NAT holds ((G1 . n) vol) . s <= ((G . n) vol) . s by A43;
then  SUM ((G1 . n) vol) <= SUM ((G . n) vol) by SUPINF_2:43;
then  SUM ((G . n) vol) = SUM ((G1 . n) vol) by A44, XXREAL_0:1;
hence  vol (G . n) = (vol (G0 . n)) + (vol (G1 . n)) by A45, XXREAL_3:4; ::_thesis: verum
end;
end;
end;
 ( (vol G) . n = vol (G . n) & (vol G0) . n = vol (G0 . n) ) by Def7;
hence  (vol G) . n = ((vol G0) . n) + ((vol G1) . n) by A38, Def7; ::_thesis: verum
end;
 for s being Element of NAT holds 0. <= (vol G0) . s by Th13;
then  vol G0 is V93() by SUPINF_2:39;
then A46: ( (vol G0) . ((pr1 H) . (k + 1)) <= (Ser (vol G0)) . ((pr1 H) . (k + 1)) & (Ser (vol G0)) . ((pr1 H) . (k + 1)) <= (Ser (vol G0)) . m ) by Th2, SUPINF_2:41;
A47: for s being Element of NAT holds
( ( s in N0 implies ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ) & ( not s in N0 implies ((On (G0,H)) vol) . s = 0. ) )
proof
let s be Element of NAT ; ::_thesis: ( ( s in N0 implies ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ) & ( not s in N0 implies ((On (G0,H)) vol) . s = 0. ) )
thus  ( s in N0 implies ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ) ::_thesis: ( not s in N0 implies ((On (G0,H)) vol) . s = 0. )
proof
assume A48: s in N0 ; ::_thesis: ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s
then A49: ex s1 being Element of NAT st
( s1 = s & (pr1 H) . (k + 1) = (pr1 H) . s1 ) ;
A50: (pr2 H) . s = SOS . s by A36, A48;
((On (G0,H)) vol) . s = diameter ((On (G0,H)) . s) by Def4
.= diameter ((G0 . ((pr1 H) . (k + 1))) . ((pr2 H) . s)) by A2, A49, Def11
.= ((G0 . ((pr1 H) . (k + 1))) vol) . (SOS . s) by A50, Def4
.= (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s by A48, FUNCT_2:15 ;
hence  ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ; ::_thesis: verum
end;
assume  not s in N0 ; ::_thesis: ((On (G0,H)) vol) . s = 0.
then A51: not (pr1 H) . (k + 1) = (pr1 H) . s ;
((On (G0,H)) vol) . s = diameter ((On (G0,H)) . s) by Def4
.= diameter ((G0 . ((pr1 H) . s)) . ((pr2 H) . s)) by A2, Def11
.= 0. by A17, A51, MEASURE5:10 ;
hence  ((On (G0,H)) vol) . s = 0. ; ::_thesis: verum
end;
 for s1, s2 being set st s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 holds
s1 = s2
proof
let s1, s2 be set ; ::_thesis: ( s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 implies s1 = s2 )
assume that
A52: ( s1 in N0 & s2 in N0 ) and
A53: SOS . s1 = SOS . s2 ; ::_thesis: s1 = s2
reconsider s1 = s1, s2 = s2 as Element of NAT by A52;
A54: ( ex s11 being Element of NAT st
( s11 = s1 & (pr1 H) . (k + 1) = (pr1 H) . s11 ) & ex s22 being Element of NAT st
( s22 = s2 & (pr1 H) . (k + 1) = (pr1 H) . s22 ) ) by A52;
A55: ( H . s1 = [((pr1 H) . s1),((pr2 H) . s1)] & H . s2 = [((pr1 H) . s2),((pr2 H) . s2)] ) by FUNCT_2:119;
 ( SOS . s1 = (pr2 H) . s1 & SOS . s2 = (pr2 H) . s2 ) by A36, A52;
hence  s1 = s2 by A1, A53, A54, A55, FUNCT_2:19; ::_thesis: verum
end;
then A56: SOS is one-to-one by FUNCT_2:19;
 (G0 . ((pr1 H) . (k + 1))) vol is V93() by Th12;
then  SUM ((On (G0,H)) vol) <= SUM ((G0 . ((pr1 H) . (k + 1))) vol) by A56, A47, Th11;
then A57: (Ser ((On (G0,H)) vol)) . (k + 1) <= SUM ((G0 . ((pr1 H) . (k + 1))) vol) by A21, XXREAL_0:2;
SUM ((G0 . ((pr1 H) . (k + 1))) vol) = vol (G0 . ((pr1 H) . (k + 1)))
.= (vol G0) . ((pr1 H) . (k + 1)) by Def7 ;
then  SUM ((G0 . ((pr1 H) . (k + 1))) vol) <= (Ser (vol G0)) . m by A46, XXREAL_0:2;
then A58: (Ser ((On (G0,H)) vol)) . (k + 1) <= (Ser (vol G0)) . m by A57, XXREAL_0:2;
 for s being Element of NAT holds 0. <= (vol G0) . s by Th13;
then  vol G0 is V93() by SUPINF_2:39;
then  (Ser (vol G)) . m = ((Ser (vol G0)) . m) + ((Ser (vol G1)) . m) by A37, A33, Th3;
hence  (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m by A58, A34, A32, XXREAL_3:36; ::_thesis: verum
end;
A59: S1[ 0 ]
proof
take m = (pr1 H) . 0; ::_thesis: for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m
let F be Function of NAT,(bool REAL); ::_thesis: for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m
let G be Interval_Covering of F; ::_thesis: (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m
reconsider GG = On (G,H) as Interval_Covering of union (rng F) ;
 ( (GG vol) . 0 = diameter (GG . 0) & ((G . ((pr1 H) . 0)) vol) . ((pr2 H) . 0) = diameter ((G . ((pr1 H) . 0)) . ((pr2 H) . 0)) ) by Def4;
then  (GG vol) . 0 <= ((G . ((pr1 H) . 0)) vol) . ((pr2 H) . 0) by A2, Def11;
then  (GG vol) . 0 <= vol (G . ((pr1 H) . 0)) by Th12, MEASURE6:3;
then A60: ( (Ser (GG vol)) . 0 = (GG vol) . 0 & (GG vol) . 0 <= (vol G) . ((pr1 H) . 0) ) by Def7, SUPINF_2:44;
 for n being Element of NAT holds 0. <= (vol G) . n by Th13;
then  vol G is V93() by SUPINF_2:39;
then  (vol G) . m <= (Ser (vol G)) . m by Th2;
hence  (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m by A60, XXREAL_0:2; ::_thesis: verum
end;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A59, A3); ::_thesis: verum
end;

theorem Th15: :: MEASURE7:15
for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F holds inf (Svc (union (rng F))) <= SUM (vol G)
proof
let F be Function of NAT,(bool REAL); ::_thesis: for G being Interval_Covering of F holds inf (Svc (union (rng F))) <= SUM (vol G)
let G be Interval_Covering of F; ::_thesis: inf (Svc (union (rng F))) <= SUM (vol G)
consider H being Function of NAT,[:NAT,NAT:] such that
A1: H is one-to-one and
 dom H = NAT and
A2: rng H = [:NAT,NAT:] by MEASURE6:1;
set GG = On (G,H);
A3: for x being ext-real number st x in rng (Ser ((On (G,H)) vol)) holds
ex y being ext-real number st
( y in rng (Ser (vol G)) & x <= y )
proof
let x be ext-real number ; ::_thesis: ( x in rng (Ser ((On (G,H)) vol)) implies ex y being ext-real number st
( y in rng (Ser (vol G)) & x <= y ) )
assume  x in rng (Ser ((On (G,H)) vol)) ; ::_thesis: ex y being ext-real number st
( y in rng (Ser (vol G)) & x <= y )
then consider n being set  such that
A4: n in dom (Ser ((On (G,H)) vol)) and
A5: x = (Ser ((On (G,H)) vol)) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A4;
consider m being Element of NAT  such that
A6: for F being Function of NAT,(bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . n <= (Ser (vol G)) . m by A1, A2, Th14;
take  (Ser (vol G)) . m ; ::_thesis: ( (Ser (vol G)) . m in rng (Ser (vol G)) & x <= (Ser (vol G)) . m )
 dom (Ser (vol G)) = NAT by FUNCT_2:def_1;
hence  ( (Ser (vol G)) . m in rng (Ser (vol G)) & x <= (Ser (vol G)) . m ) by A5, A6, FUNCT_1:def_3; ::_thesis: verum
end;
set Q = vol (On (G,H));
 vol (On (G,H)) in Svc (union (rng F)) by Def8;
then A7: inf (Svc (union (rng F))) <= vol (On (G,H)) by XXREAL_2:3;
 ( SUM ((On (G,H)) vol) = sup (rng (Ser ((On (G,H)) vol))) & SUM (vol G) = sup (rng (Ser (vol G))) ) by SUPINF_2:def_17;
then  vol (On (G,H)) <= SUM (vol G) by A3, XXREAL_2:63;
hence  inf (Svc (union (rng F))) <= SUM (vol G) by A7, XXREAL_0:2; ::_thesis: verum
end;

theorem Th16: :: MEASURE7:16
OS_Meas is C_Measure of REAL
proof
set G = D;
 ( {} c= union (rng D) & ( for n being Element of NAT holds D . n is Interval ) ) by FUNCOP_1:7, XBOOLE_1:2;
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 V93()
proof
let A be Subset of REAL; ::_thesis: for F being Interval_Covering of A holds F vol is V93()
let F be Interval_Covering of A; ::_thesis: F vol is V93()
 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 V93() 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 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;
set y = (Ser (F vol)) . 0;
 F vol is V93() 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, SUPINF_2:def_17, 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 V93() by MEASURE1:def_2; :: according to MEASURE4:def_1 ::_thesis: ( OS_Meas is V76() & ( for b1, b2 being Element of bool REAL holds
( not b1 c= b2 or ( OS_Meas . b1 <= OS_Meas . b2 & ( for b3 being Element of bool [:NAT,(bool REAL):] holds OS_Meas . (union (rng b3)) <= SUM (OS_Meas * b3) ) ) ) ) )
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:44
.= 0. by A6 ;
then A7: 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  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 b1, b2 being Element of bool REAL holds
( not b1 c= b2 or ( OS_Meas . b1 <= OS_Meas . b2 & ( for b3 being Element of bool [:NAT,(bool REAL):] holds OS_Meas . (union (rng b3)) <= SUM (OS_Meas * b3) ) ) )
let A, B be Subset of REAL; ::_thesis: ( not A c= B or ( OS_Meas . A <= OS_Meas . B & ( for b1 being Element of bool [:NAT,(bool REAL):] holds OS_Meas . (union (rng b1)) <= SUM (OS_Meas * b1) ) ) )
assume A9: A c= B ; ::_thesis: ( OS_Meas . A <= OS_Meas . B & ( for b1 being Element of bool [:NAT,(bool REAL):] holds OS_Meas . (union (rng b1)) <= SUM (OS_Meas * b1) ) )
A10: 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 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, XBOOLE_1:1;
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 b1 being Element of bool [:NAT,(bool REAL):] holds OS_Meas . (union (rng b1)) <= SUM (OS_Meas * b1)
let F be Function of NAT,(bool REAL); ::_thesis: OS_Meas . (union (rng F)) <= SUM (OS_Meas * F)
percases ( for n being Element of NAT holds Svc (F . n) <> {+infty} or ex n being Element of NAT st Svc (F . n) = {+infty} ) ;
supposeA14: for n being Element of NAT holds Svc (F . n) <> {+infty} ; ::_thesis: OS_Meas . (union (rng F)) <= SUM (OS_Meas * F)
A15: SUM (OS_Meas * F) = sup (rng (Ser (OS_Meas * F))) by SUPINF_2:def_17;
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 V93() 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:44;
 (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 number  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 Function of NAT,ExtREAL such that
A22: for n being Element of 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 S1[ 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 S1[n,F0]
proof
let n be Element of NAT ; ::_thesis: ex F0 being Element of Funcs (NAT,(bool REAL)) st S1[n,F0]
A26: ( OS_Meas . (F . n) = inf (Svc (F . n)) & 0 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 set  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 Real by A2, A26, XXREAL_0:46;
then consider S being ext-real number  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: S1[n,FS]
thus  S1[n,FS] by A30, A31; ::_thesis: verum
end;
consider FF being Function of NAT,(Funcs (NAT,(bool REAL))) such that
A32: for n being Element of NAT holds S1[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 S2[ 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 S2[n,y] ;
consider G0 being Function of NAT,ExtREAL such that
A35: for n being Element of NAT holds S2[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 V93() 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 A15, A21, A33, XXREAL_0:2; ::_thesis: verum
end;
hence  OS_Meas . (union (rng F)) <= SUM (OS_Meas * F) by A15, 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 V93() 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;
end;

definition
:: original: OS_Meas
redefine func OS_Meas  ->  C_Measure of REAL ;
correctness
coherence
OS_Meas is C_Measure of REAL ;
by Th16;
end;

definition
func Lmi_sigmaFIELD  ->  SigmaField of REAL equals :: MEASURE7:def 12
 sigma_Field OS_Meas;
coherence
 sigma_Field OS_Meas is SigmaField of REAL ;
end;

:: deftheorem  defines Lmi_sigmaFIELD MEASURE7:def_12_:_
 Lmi_sigmaFIELD = sigma_Field OS_Meas;

definition
func L_mi  ->  sigma_Measure of Lmi_sigmaFIELD equals :: MEASURE7:def 13
 sigma_Meas OS_Meas;
correctness
coherence
sigma_Meas OS_Meas is sigma_Measure of Lmi_sigmaFIELD;
;
end;

:: deftheorem  defines L_mi MEASURE7:def_13_:_
 L_mi = sigma_Meas OS_Meas;