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 = lower_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds
( lower_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 = lower_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds
( lower_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 = lower_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds
( lower_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 = lower_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds
( lower_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 = lower_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 = lower_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds
( lower_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 = lower_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds
( lower_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 = lower_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds
( lower_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 = lower_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds
( lower_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 = lower_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds
( lower_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 = lower_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds
( lower_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 = lower_bound (rng (f | (divset (D,k)))) ) by A9; :: thesis: ( dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds
( lower_bound (rng f) <= g . x & g . x <= f . x ) ) )

thus dom g = A by A8; :: thesis: ( Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds
( lower_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 A11: B-Meas . A = b1 - a1 by ;
then A12: B-Meas . A1 < +infty by XXREAL_0:4;
defpred S1[ Nat, ExtReal] means ( \$2 = lower_bound (rng (f | (divset (D,\$1)))) & \$2 is Real );
A13: 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]
reconsider r = lower_bound (rng (f | (divset (D,k)))) as Element of ExtREAL by XXREAL_0:def 1;
take r ; :: thesis: S1[k,r]
thus S1[k,r] ; :: thesis: verum
end;
consider h being FinSequence of ExtREAL such that
A14: ( dom h = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S1[k,h . k] ) ) from A15: dom h = dom F by ;
A16: 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 A17: k in dom F ; :: thesis: for x being object st x in F . k holds
g . x = h . k

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

thus for x being Real st x in A holds
( lower_bound (rng f) <= g . x & g . x <= f . x ) :: thesis: verum
proof
let x be Real; :: thesis: ( x in A implies ( lower_bound (rng f) <= g . x & g . x <= f . x ) )
assume A53: x in A ; :: thesis: ( lower_bound (rng f) <= g . x & g . x <= f . x )
then consider k being Nat such that
A54: ( 1 <= k & k <= len F & x in F . k & g . x = lower_bound (rng (f | (divset (D,k)))) ) by A8, A9;
A55: k in dom F by ;
A56: F . k c= divset (D,k)
proof
per cases ( len D = 1 or len D <> 1 ) ;
suppose A57: len D = 1 ; :: thesis: F . k c= divset (D,k)
then A58: 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 A59: 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 A60: 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 A61: divset (D,k) = [.a,(D . k).] by ;
F . k = [.a,(D . k).[ by A55, A59, A60, A6;
hence F . k c= divset (D,k) by ; :: thesis: verum
end;
suppose A62: 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 A63: 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 A55, A59, A62, A6, A63; :: thesis: verum
end;
suppose A64: ( 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 A65: divset (D,k) = [.(D . (k - 1)),(D . k).] by INTEGRA1:4;
len D = len F by ;
then A66: ( 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 A55, A66, A6;
hence F . k c= divset (D,k) by ; :: thesis: verum
end;
end;
end;
end;
end;
then A67: x in dom (f | (divset (D,k))) by ;
divset (D,k) c= A by ;
then A68: divset (D,k) c= dom f by A2;
A69: rng f is bounded_below by ;
f = f | (dom f) ;
then f | (divset (D,k)) is bounded by ;
then A70: 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 ( lower_bound (rng f) <= g . x & g . x <= f . x ) by ; :: thesis: verum
end;