let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of A,REAL
for D being Division of A st f is bounded & A c= dom f holds
ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )

let f be PartFunc of A,REAL; :: thesis: for D being Division of A st f is bounded & A c= dom f holds
ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )

let D be Division of A; :: thesis: ( f is bounded & A c= dom f implies ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) ) )

assume that
A1: f is bounded and
A2: A c= dom f ; :: thesis: ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )

consider a, b being Real such that
A3: ( a <= b & A = [.a,b.] ) by MEASURE5:14;
reconsider a1 = a, b1 = b as R_eal by XXREAL_0:def 1;
consider F being Finite_Sep_Sequence of Borel_Sets , g being PartFunc of REAL,ExtREAL such that
A4: dom F = dom D and
A5: union (rng F) = A and
A6: for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) and
A7: g is_simple_func_in Borel_Sets and
A8: dom g = A and
A9: for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) by ;
A = [.(),().] by INTEGRA1:4;
then A10: ( inf A = a & sup A = b ) by ;
take F ; :: thesis: ex g being PartFunc of REAL,ExtREAL st
( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )

take g ; :: thesis: ( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )

thus dom F = dom D by A4; :: thesis: ( union (rng F) = A & ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )

thus union (rng F) = A by A5; :: thesis: ( ( for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )

thus for k being Nat st k in dom F holds
( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) by ; :: thesis: ( g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )

thus g is_simple_func_in Borel_Sets by A7; :: thesis: ( ( for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )

thus for x being Real st x in dom g holds
ex k being Nat st
( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) by A9; :: thesis: ( dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )

thus dom g = A by A8; :: thesis: ( Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )

reconsider A1 = A as Element of Borel_Sets by MEASUR12:72;
B-Meas . A = diameter A by MEASUR12:71;
then B-Meas . A = b1 - a1 by ;
then A11: B-Meas . A1 < +infty by XXREAL_0:4;
defpred S1[ Nat, ExtReal] means ( \$2 = upper_bound (rng (f | (divset (D,\$1)))) & \$2 is Real );
A12: for k being Nat st k in Seg (len F) holds
ex r being Element of ExtREAL st S1[k,r]
proof
let k be Nat; :: thesis: ( k in Seg (len F) implies ex r being Element of ExtREAL st S1[k,r] )
assume k in Seg (len F) ; :: thesis: ex r being Element of ExtREAL st S1[k,r]
upper_bound (rng (f | (divset (D,k)))) is Element of ExtREAL by XXREAL_0:def 1;
hence ex r being Element of ExtREAL st S1[k,r] ; :: thesis: verum
end;
consider h being FinSequence of ExtREAL such that
A13: ( dom h = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S1[k,h . k] ) ) from A14: dom h = dom F by ;
A15: for k being Nat st k in dom F holds
for x being object st x in F . k holds
g . x = h . k
proof
let k be Nat; :: thesis: ( k in dom F implies for x being object st x in F . k holds
g . x = h . k )

assume A16: k in dom F ; :: thesis: for x being object st x in F . k holds
g . x = h . k

then A17: F . k in rng F by FUNCT_1:3;
let x be object ; :: thesis: ( x in F . k implies g . x = h . k )
assume A18: x in F . k ; :: thesis: g . x = h . k
then x in dom g by ;
then consider i being Nat such that
A19: ( 1 <= i & i <= len F & x in F . i & g . x = upper_bound (rng (f | (divset (D,i)))) ) by A9;
k = i by ;
hence g . x = h . k by A19, A13, A16, A14; :: thesis: verum
end;
defpred S2[ Nat, ExtReal] means ( \$2 = (h . \$1) * (() . \$1) & \$2 is Real );
A20: for k being Nat st k in Seg (len F) holds
ex r being Element of ExtREAL st S2[k,r]
proof
let k be Nat; :: thesis: ( k in Seg (len F) implies ex r being Element of ExtREAL st S2[k,r] )
assume A21: k in Seg (len F) ; :: thesis: ex r being Element of ExtREAL st S2[k,r]
then A22: ( h . k = upper_bound (rng (f | (divset (D,k)))) & h . k is Real ) by A13;
A23: F . k c= A by ;
F . k in Borel_Sets by ;
then ( 0 <= B-Meas . (F . k) & B-Meas . (F . k) <= B-Meas . A1 ) by ;
then ( 0 <= B-Meas . (F . k) & B-Meas . (F . k) < +infty ) by ;
then ( 0 <= () . k & () . k < +infty ) by ;
then (B-Meas * F) . k in REAL by XXREAL_0:14;
hence ex r being Element of ExtREAL st S2[k,r] by A22; :: thesis: verum
end;
consider z being FinSequence of ExtREAL such that
A24: ( dom z = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S2[k,z . k] ) ) from A25: dom z = dom F by ;
for k being Nat st k in dom z holds
z . k = (h . k) * (() . k) by A24;
then A26: Integral (B-Meas,g) = Sum z by ;
len (upper_volume (f,D)) = len D by INTEGRA1:def 6;
then A27: dom z = dom (upper_volume (f,D)) by ;
A28: A = [.(),().] by INTEGRA1:4;
then A29: ( lower_bound A = a & upper_bound A = b ) by ;
for p being object st p in dom z holds
z . p = (upper_volume (f,D)) . p
proof
let p be object ; :: thesis: ( p in dom z implies z . p = (upper_volume (f,D)) . p )
assume A30: p in dom z ; :: thesis: z . p = (upper_volume (f,D)) . p
then reconsider p1 = p as Nat ;
A31: (B-Meas * F) . p1 = vol (divset (D,p1))
proof
per cases ( len D = 1 or len D <> 1 ) ;
suppose A32: len D = 1 ; :: thesis: () . p1 = vol (divset (D,p1))
then F . p1 = [.a,b.] by A30, A25, A6;
then B-Meas . (F . p1) = b - a by ;
then A33: (B-Meas * F) . p1 = b - a by ;
( 1 <= p1 & p1 <= 1 ) by ;
then p1 = 1 by XXREAL_0:1;
then ( lower_bound (divset (D,p1)) = lower_bound A & upper_bound (divset (D,p1)) = D . (len D) ) by ;
then ( lower_bound (divset (D,p1)) = a & upper_bound (divset (D,p1)) = b ) by ;
hence (B-Meas * F) . p1 = vol (divset (D,p1)) by ; :: thesis: verum
end;
suppose A34: len D <> 1 ; :: thesis: () . p1 = vol (divset (D,p1))
( D . p1 in rng D & rng D c= A ) by ;
then A35: ( a <= D . p1 & D . p1 <= b ) by ;
per cases ( p1 = 1 or p1 = len D or ( p1 <> 1 & p1 <> len D ) ) ;
suppose A36: p1 = 1 ; :: thesis: () . p1 = vol (divset (D,p1))
then F . p1 = [.a,(D . 1).[ by A6, A30, A25, A34;
then B-Meas . (F . p1) = (D . 1) - a by ;
then A37: (B-Meas * F) . p1 = (D . 1) - a by ;
( lower_bound (divset (D,p1)) = a & upper_bound (divset (D,p1)) = D . 1 ) by ;
hence (B-Meas * F) . p1 = vol (divset (D,p1)) by ; :: thesis: verum
end;
suppose A38: p1 = len D ; :: thesis: () . p1 = vol (divset (D,p1))
len D >= 1 by FINSEQ_1:20;
then len D > 1 by ;
then A39: p1 -' 1 >= 1 by ;
then A40: p1 -' 1 = p1 - 1 by NAT_D:39;
then A41: F . p1 = [.(D . (p1 - 1)),(D . p1).] by A6, A30, A25, A34, A38;
p1 -' 1 in dom D by ;
then D . (p1 - 1) <= D . p1 by ;
then B-Meas . (F . p1) = (D . p1) - (D . (p1 - 1)) by ;
then A42: (B-Meas * F) . p1 = (D . p1) - (D . (p1 - 1)) by ;
( lower_bound (divset (D,p1)) = D . (p1 - 1) & upper_bound (divset (D,p1)) = D . p1 ) by ;
hence (B-Meas * F) . p1 = vol (divset (D,p1)) by ; :: thesis: verum
end;
suppose A43: ( p1 <> 1 & p1 <> len D ) ; :: thesis: () . p1 = vol (divset (D,p1))
( 1 <= p1 & p1 <= len D ) by ;
then A44: ( 1 < p1 & p1 < len D ) by ;
then A45: F . p1 = [.(D . (p1 -' 1)),(D . p1).[ by A6, A30, A25;
A46: 1 <= p1 -' 1 by ;
then A47: p1 -' 1 = p1 - 1 by NAT_D:39;
p1 - 1 <= p1 by XREAL_1:43;
then p1 -' 1 < len D by ;
then p1 -' 1 in dom D by ;
then D . (p1 -' 1) <= D . p1 by ;
then B-Meas . (F . p1) = (D . p1) - (D . (p1 - 1)) by ;
then A48: (B-Meas * F) . p1 = (D . p1) - (D . (p1 - 1)) by ;
( lower_bound (divset (D,p1)) = D . (p1 - 1) & upper_bound (divset (D,p1)) = D . p1 ) by ;
hence (B-Meas * F) . p1 = vol (divset (D,p1)) by ; :: thesis: verum
end;
end;
end;
end;
end;
A49: h . p1 = upper_bound (rng (f | (divset (D,p1)))) by ;
z . p = (h . p1) * (() . p1) by ;
then z . p = (upper_bound (rng (f | (divset (D,p1))))) * (vol (divset (D,p1))) by ;
hence z . p = (upper_volume (f,D)) . p by ; :: thesis: verum
end;
then Sum z = Sum (upper_volume (f,D)) by ;
hence Integral (B-Meas,g) = upper_sum (f,D) by ; :: thesis: for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x )

thus for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) :: thesis: verum
proof
let x be Real; :: thesis: ( x in A implies ( upper_bound (rng f) >= g . x & g . x >= f . x ) )
assume A50: x in A ; :: thesis: ( upper_bound (rng f) >= g . x & g . x >= f . x )
then consider k being Nat such that
A51: ( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) by A8, A9;
A52: k in dom F by ;
A53: F . k c= divset (D,k)
proof
per cases ( len D = 1 or len D <> 1 ) ;
suppose A54: len D = 1 ; :: thesis: F . k c= divset (D,k)
then A55: F . k = [.a,b.] by ;
len D = len F by ;
then k = 1 by ;
then ( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = D . 1 ) by ;
then ( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = upper_bound A ) by ;
hence F . k c= divset (D,k) by ; :: thesis: verum
end;
suppose A56: len D <> 1 ; :: thesis: F . k c= divset (D,k)
per cases ( k = 1 or k = len D or ( k <> 1 & k <> len D ) ) ;
suppose A57: k = 1 ; :: thesis: F . k c= divset (D,k)
then ( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = D . k ) by ;
then A58: divset (D,k) = [.a,(D . k).] by ;
F . k = [.a,(D . k).[ by A52, A56, A57, A6;
hence F . k c= divset (D,k) by ; :: thesis: verum
end;
suppose A59: k = len D ; :: thesis: F . k c= divset (D,k)
then ( lower_bound (divset (D,k)) = D . (k - 1) & upper_bound (divset (D,k)) = D . k ) by ;
then A60: divset (D,k) = [.(D . (k - 1)),(D . k).] by INTEGRA1:4;
1 < k by ;
then 1 <= k -' 1 by NAT_D:49;
then k -' 1 = k - 1 by NAT_D:39;
hence F . k c= divset (D,k) by A52, A56, A59, A6, A60; :: thesis: verum
end;
suppose A61: ( k <> 1 & k <> len D ) ; :: thesis: F . k c= divset (D,k)
then ( lower_bound (divset (D,k)) = D . (k - 1) & upper_bound (divset (D,k)) = D . k ) by ;
then A62: divset (D,k) = [.(D . (k - 1)),(D . k).] by INTEGRA1:4;
len D = len F by ;
then A63: ( 1 < k & k < len D ) by ;
then 1 <= k -' 1 by NAT_D:49;
then k -' 1 = k - 1 by NAT_D:39;
then F . k = [.(D . (k - 1)),(D . k).[ by A52, A63, A6;
hence F . k c= divset (D,k) by ; :: thesis: verum
end;
end;
end;
end;
end;
then A64: x in dom (f | (divset (D,k))) by ;
divset (D,k) c= A by ;
then A65: divset (D,k) c= dom f by A2;
A66: rng f is bounded_above by ;
f = f | (dom f) ;
then f | (divset (D,k)) is bounded by ;
then A67: rng (f | (divset (D,k))) is real-bounded by INTEGRA1:15;
(f | (divset (D,k))) . x = f . x by ;
then f . x in rng (f | (divset (D,k))) by ;
hence ( upper_bound (rng f) >= g . x & g . x >= f . x ) by ; :: thesis: verum
end;