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 A3, Th11;

A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;

then A10: ( inf A = a & sup A = b ) by A3, INTEGRA1:5;

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 A6, A10; :: 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 A3, MEASURE5:6;

then A11: B-Meas . A1 < +infty by XXREAL_0:4;

defpred S_{1}[ 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 S_{1}[k,r]

A13: ( dom h = Seg (len F) & ( for k being Nat st k in Seg (len F) holds

S_{1}[k,h . k] ) )
from FINSEQ_1:sch 5(A12);

A14: dom h = dom F by A13, FINSEQ_1:def 3;

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_{2}[ Nat, ExtReal] means ( $2 = (h . $1) * ((B-Meas * F) . $1) & $2 is Real );

A20: for k being Nat st k in Seg (len F) holds

ex r being Element of ExtREAL st S_{2}[k,r]

A24: ( dom z = Seg (len F) & ( for k being Nat st k in Seg (len F) holds

S_{2}[k,z . k] ) )
from FINSEQ_1:sch 5(A20);

A25: dom z = dom F by A24, FINSEQ_1:def 3;

for k being Nat st k in dom z holds

z . k = (h . k) * ((B-Meas * F) . k) by A24;

then A26: Integral (B-Meas,g) = Sum z by A5, A8, A14, A7, A11, A15, A25, Th18, MESFUNC3:def 1;

len (upper_volume (f,D)) = len D by INTEGRA1:def 6;

then A27: dom z = dom (upper_volume (f,D)) by A25, A4, FINSEQ_3:29;

A28: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;

then A29: ( lower_bound A = a & upper_bound A = b ) by A3, INTEGRA1:5;

for p being object st p in dom z holds

z . p = (upper_volume (f,D)) . p

hence Integral (B-Meas,g) = upper_sum (f,D) by A26, INTEGRA1:def 8; :: 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

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 A3, Th11;

A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;

then A10: ( inf A = a & sup A = b ) by A3, INTEGRA1:5;

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 A6, A10; :: 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 A3, MEASURE5:6;

then A11: B-Meas . A1 < +infty by XXREAL_0:4;

defpred S

A12: for k being Nat st k in Seg (len F) holds

ex r being Element of ExtREAL st S

proof

consider h being FinSequence of ExtREAL such that
let k be Nat; :: thesis: ( k in Seg (len F) implies ex r being Element of ExtREAL st S_{1}[k,r] )

assume k in Seg (len F) ; :: thesis: ex r being Element of ExtREAL st S_{1}[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 S_{1}[k,r]
; :: thesis: verum

end;assume k in Seg (len F) ; :: thesis: ex r being Element of ExtREAL st S

upper_bound (rng (f | (divset (D,k)))) is Element of ExtREAL by XXREAL_0:def 1;

hence ex r being Element of ExtREAL st S

A13: ( dom h = Seg (len F) & ( for k being Nat st k in Seg (len F) holds

S

A14: dom h = dom F by A13, FINSEQ_1:def 3;

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

defpred S
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 A5, A8, A17, TARSKI:def 4;

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 A18, A19, XBOOLE_0:3, PROB_2:def 2;

hence g . x = h . k by A19, A13, A16, A14; :: thesis: verum

end;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 A5, A8, A17, TARSKI:def 4;

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 A18, A19, XBOOLE_0:3, PROB_2:def 2;

hence g . x = h . k by A19, A13, A16, A14; :: thesis: verum

A20: for k being Nat st k in Seg (len F) holds

ex r being Element of ExtREAL st S

proof

consider z being FinSequence of ExtREAL such that
let k be Nat; :: thesis: ( k in Seg (len F) implies ex r being Element of ExtREAL st S_{2}[k,r] )

assume A21: k in Seg (len F) ; :: thesis: ex r being Element of ExtREAL st S_{2}[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 A5, A21, A14, A13, FUNCT_1:3, ZFMISC_1:74;

F . k in Borel_Sets by A21, A14, A13, PARTFUN1:4;

then ( 0 <= B-Meas . (F . k) & B-Meas . (F . k) <= B-Meas . A1 ) by A23, SUPINF_2:51, MEASURE1:31;

then ( 0 <= B-Meas . (F . k) & B-Meas . (F . k) < +infty ) by A11, XXREAL_0:4;

then ( 0 <= (B-Meas * F) . k & (B-Meas * F) . k < +infty ) by A21, A13, A14, FUNCT_1:13;

then (B-Meas * F) . k in REAL by XXREAL_0:14;

hence ex r being Element of ExtREAL st S_{2}[k,r]
by A22; :: thesis: verum

end;assume A21: k in Seg (len F) ; :: thesis: ex r being Element of ExtREAL st S

then A22: ( h . k = upper_bound (rng (f | (divset (D,k)))) & h . k is Real ) by A13;

A23: F . k c= A by A5, A21, A14, A13, FUNCT_1:3, ZFMISC_1:74;

F . k in Borel_Sets by A21, A14, A13, PARTFUN1:4;

then ( 0 <= B-Meas . (F . k) & B-Meas . (F . k) <= B-Meas . A1 ) by A23, SUPINF_2:51, MEASURE1:31;

then ( 0 <= B-Meas . (F . k) & B-Meas . (F . k) < +infty ) by A11, XXREAL_0:4;

then ( 0 <= (B-Meas * F) . k & (B-Meas * F) . k < +infty ) by A21, A13, A14, FUNCT_1:13;

then (B-Meas * F) . k in REAL by XXREAL_0:14;

hence ex r being Element of ExtREAL st S

A24: ( dom z = Seg (len F) & ( for k being Nat st k in Seg (len F) holds

S

A25: dom z = dom F by A24, FINSEQ_1:def 3;

for k being Nat st k in dom z holds

z . k = (h . k) * ((B-Meas * F) . k) by A24;

then A26: Integral (B-Meas,g) = Sum z by A5, A8, A14, A7, A11, A15, A25, Th18, MESFUNC3:def 1;

len (upper_volume (f,D)) = len D by INTEGRA1:def 6;

then A27: dom z = dom (upper_volume (f,D)) by A25, A4, FINSEQ_3:29;

A28: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;

then A29: ( lower_bound A = a & upper_bound A = b ) by A3, INTEGRA1:5;

for p being object st p in dom z holds

z . p = (upper_volume (f,D)) . p

proof

then
Sum z = Sum (upper_volume (f,D))
by A27, FUNCT_1:2, MESFUNC3:2;
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))

z . p = (h . p1) * ((B-Meas * F) . p1) by A24, A30;

then z . p = (upper_bound (rng (f | (divset (D,p1))))) * (vol (divset (D,p1))) by A31, A49, XXREAL_3:def 5;

hence z . p = (upper_volume (f,D)) . p by A30, A25, A4, INTEGRA1:def 6; :: thesis: verum

end;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
end;

A49:
h . p1 = upper_bound (rng (f | (divset (D,p1))))
by A30, A13, A24;per cases
( len D = 1 or len D <> 1 )
;

end;

suppose A32:
len D = 1
; :: thesis: (B-Meas * F) . p1 = vol (divset (D,p1))

then
F . p1 = [.a,b.]
by A30, A25, A6;

then B-Meas . (F . p1) = b - a by A3, Th5;

then A33: (B-Meas * F) . p1 = b - a by A30, A25, FUNCT_1:13;

( 1 <= p1 & p1 <= 1 ) by A30, A25, A4, A32, FINSEQ_3:25;

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 A30, A25, A4, A32, INTEGRA1:def 4;

then ( lower_bound (divset (D,p1)) = a & upper_bound (divset (D,p1)) = b ) by A29, INTEGRA1:def 2;

hence (B-Meas * F) . p1 = vol (divset (D,p1)) by A33, INTEGRA1:def 5; :: thesis: verum

end;then B-Meas . (F . p1) = b - a by A3, Th5;

then A33: (B-Meas * F) . p1 = b - a by A30, A25, FUNCT_1:13;

( 1 <= p1 & p1 <= 1 ) by A30, A25, A4, A32, FINSEQ_3:25;

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 A30, A25, A4, A32, INTEGRA1:def 4;

then ( lower_bound (divset (D,p1)) = a & upper_bound (divset (D,p1)) = b ) by A29, INTEGRA1:def 2;

hence (B-Meas * F) . p1 = vol (divset (D,p1)) by A33, INTEGRA1:def 5; :: thesis: verum

suppose A34:
len D <> 1
; :: thesis: (B-Meas * F) . p1 = vol (divset (D,p1))

( D . p1 in rng D & rng D c= A )
by A30, A25, A4, FUNCT_1:3, INTEGRA1:def 2;

then A35: ( a <= D . p1 & D . p1 <= b ) by A3, XXREAL_1:1;

end;then A35: ( a <= D . p1 & D . p1 <= b ) by A3, XXREAL_1:1;

per cases
( p1 = 1 or p1 = len D or ( p1 <> 1 & p1 <> len D ) )
;

end;

suppose A36:
p1 = 1
; :: thesis: (B-Meas * F) . 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 A35, A36, Th5;

then A37: (B-Meas * F) . p1 = (D . 1) - a by A30, A25, FUNCT_1:13;

( lower_bound (divset (D,p1)) = a & upper_bound (divset (D,p1)) = D . 1 ) by A29, A30, A25, A4, A36, INTEGRA1:def 4;

hence (B-Meas * F) . p1 = vol (divset (D,p1)) by A37, INTEGRA1:def 5; :: thesis: verum

end;then B-Meas . (F . p1) = (D . 1) - a by A35, A36, Th5;

then A37: (B-Meas * F) . p1 = (D . 1) - a by A30, A25, FUNCT_1:13;

( lower_bound (divset (D,p1)) = a & upper_bound (divset (D,p1)) = D . 1 ) by A29, A30, A25, A4, A36, INTEGRA1:def 4;

hence (B-Meas * F) . p1 = vol (divset (D,p1)) by A37, INTEGRA1:def 5; :: thesis: verum

suppose A38:
p1 = len D
; :: thesis: (B-Meas * F) . p1 = vol (divset (D,p1))

len D >= 1
by FINSEQ_1:20;

then len D > 1 by A34, XXREAL_0:1;

then A39: p1 -' 1 >= 1 by A38, NAT_D:49;

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 A39, A38, A40, FINSEQ_3:25, XREAL_1:43;

then D . (p1 - 1) <= D . p1 by A40, A30, A25, A4, VALUED_0:def 15, XREAL_1:43;

then B-Meas . (F . p1) = (D . p1) - (D . (p1 - 1)) by A41, Th5;

then A42: (B-Meas * F) . p1 = (D . p1) - (D . (p1 - 1)) by A30, A25, FUNCT_1:13;

( lower_bound (divset (D,p1)) = D . (p1 - 1) & upper_bound (divset (D,p1)) = D . p1 ) by A30, A25, A4, A38, A34, INTEGRA1:def 4;

hence (B-Meas * F) . p1 = vol (divset (D,p1)) by A42, INTEGRA1:def 5; :: thesis: verum

end;then len D > 1 by A34, XXREAL_0:1;

then A39: p1 -' 1 >= 1 by A38, NAT_D:49;

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 A39, A38, A40, FINSEQ_3:25, XREAL_1:43;

then D . (p1 - 1) <= D . p1 by A40, A30, A25, A4, VALUED_0:def 15, XREAL_1:43;

then B-Meas . (F . p1) = (D . p1) - (D . (p1 - 1)) by A41, Th5;

then A42: (B-Meas * F) . p1 = (D . p1) - (D . (p1 - 1)) by A30, A25, FUNCT_1:13;

( lower_bound (divset (D,p1)) = D . (p1 - 1) & upper_bound (divset (D,p1)) = D . p1 ) by A30, A25, A4, A38, A34, INTEGRA1:def 4;

hence (B-Meas * F) . p1 = vol (divset (D,p1)) by A42, INTEGRA1:def 5; :: thesis: verum

suppose A43:
( p1 <> 1 & p1 <> len D )
; :: thesis: (B-Meas * F) . p1 = vol (divset (D,p1))

( 1 <= p1 & p1 <= len D )
by A30, A25, A4, FINSEQ_3:25;

then A44: ( 1 < p1 & p1 < len D ) by A43, XXREAL_0:1;

then A45: F . p1 = [.(D . (p1 -' 1)),(D . p1).[ by A6, A30, A25;

A46: 1 <= p1 -' 1 by A44, NAT_D:49;

then A47: p1 -' 1 = p1 - 1 by NAT_D:39;

p1 - 1 <= p1 by XREAL_1:43;

then p1 -' 1 < len D by A44, A47, XXREAL_0:2;

then p1 -' 1 in dom D by A46, FINSEQ_3:25;

then D . (p1 -' 1) <= D . p1 by A47, A30, A25, A4, VALUED_0:def 15, XREAL_1:43;

then B-Meas . (F . p1) = (D . p1) - (D . (p1 - 1)) by A45, A47, Th5;

then A48: (B-Meas * F) . p1 = (D . p1) - (D . (p1 - 1)) by A30, A25, FUNCT_1:13;

( lower_bound (divset (D,p1)) = D . (p1 - 1) & upper_bound (divset (D,p1)) = D . p1 ) by A30, A25, A4, A43, INTEGRA1:def 4;

hence (B-Meas * F) . p1 = vol (divset (D,p1)) by A48, INTEGRA1:def 5; :: thesis: verum

end;then A44: ( 1 < p1 & p1 < len D ) by A43, XXREAL_0:1;

then A45: F . p1 = [.(D . (p1 -' 1)),(D . p1).[ by A6, A30, A25;

A46: 1 <= p1 -' 1 by A44, NAT_D:49;

then A47: p1 -' 1 = p1 - 1 by NAT_D:39;

p1 - 1 <= p1 by XREAL_1:43;

then p1 -' 1 < len D by A44, A47, XXREAL_0:2;

then p1 -' 1 in dom D by A46, FINSEQ_3:25;

then D . (p1 -' 1) <= D . p1 by A47, A30, A25, A4, VALUED_0:def 15, XREAL_1:43;

then B-Meas . (F . p1) = (D . p1) - (D . (p1 - 1)) by A45, A47, Th5;

then A48: (B-Meas * F) . p1 = (D . p1) - (D . (p1 - 1)) by A30, A25, FUNCT_1:13;

( lower_bound (divset (D,p1)) = D . (p1 - 1) & upper_bound (divset (D,p1)) = D . p1 ) by A30, A25, A4, A43, INTEGRA1:def 4;

hence (B-Meas * F) . p1 = vol (divset (D,p1)) by A48, INTEGRA1:def 5; :: thesis: verum

z . p = (h . p1) * ((B-Meas * F) . p1) by A24, A30;

then z . p = (upper_bound (rng (f | (divset (D,p1))))) * (vol (divset (D,p1))) by A31, A49, XXREAL_3:def 5;

hence z . p = (upper_volume (f,D)) . p by A30, A25, A4, INTEGRA1:def 6; :: thesis: verum

hence Integral (B-Meas,g) = upper_sum (f,D) by A26, INTEGRA1:def 8; :: 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 A51, FINSEQ_3:25;

A53: F . k c= divset (D,k)

divset (D,k) c= A by A52, A4, INTEGRA1:8;

then A65: divset (D,k) c= dom f by A2;

A66: rng f is bounded_above by A1, SEQ_2:def 8, INTEGRA1:13;

f = f | (dom f) ;

then f | (divset (D,k)) is bounded by A1, A65, RFUNCT_1:74;

then A67: rng (f | (divset (D,k))) is real-bounded by INTEGRA1:15;

(f | (divset (D,k))) . x = f . x by A51, A53, FUNCT_1:49;

then f . x in rng (f | (divset (D,k))) by A64, FUNCT_1:3;

hence ( upper_bound (rng f) >= g . x & g . x >= f . x ) by A66, A51, A67, SEQ_4:def 1, SEQ_4:48, RELAT_1:70; :: thesis: verum

end;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 A51, FINSEQ_3:25;

A53: F . k c= divset (D,k)

proof
end;

then A64:
x in dom (f | (divset (D,k)))
by A51, A2, A50, RELAT_1:57;per cases
( len D = 1 or len D <> 1 )
;

end;

suppose A54:
len D = 1
; :: thesis: F . k c= divset (D,k)

then A55:
F . k = [.a,b.]
by A6, A52;

len D = len F by A4, FINSEQ_3:29;

then k = 1 by A51, A54, XXREAL_0:1;

then ( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = D . 1 ) by A52, A4, INTEGRA1:def 4;

then ( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = upper_bound A ) by A54, INTEGRA1:def 2;

hence F . k c= divset (D,k) by A55, A28, A3, INTEGRA1:4; :: thesis: verum

end;len D = len F by A4, FINSEQ_3:29;

then k = 1 by A51, A54, XXREAL_0:1;

then ( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = D . 1 ) by A52, A4, INTEGRA1:def 4;

then ( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = upper_bound A ) by A54, INTEGRA1:def 2;

hence F . k c= divset (D,k) by A55, A28, A3, INTEGRA1:4; :: thesis: verum

suppose A56:
len D <> 1
; :: thesis: F . k c= divset (D,k)

end;

per cases
( k = 1 or k = len D or ( k <> 1 & k <> len D ) )
;

end;

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 A52, A4, INTEGRA1:def 4;

then A58: divset (D,k) = [.a,(D . k).] by A29, INTEGRA1:4;

F . k = [.a,(D . k).[ by A52, A56, A57, A6;

hence F . k c= divset (D,k) by A58, XXREAL_1:24; :: thesis: verum

end;then A58: divset (D,k) = [.a,(D . k).] by A29, INTEGRA1:4;

F . k = [.a,(D . k).[ by A52, A56, A57, A6;

hence F . k c= divset (D,k) by A58, XXREAL_1:24; :: thesis: verum

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 A52, A4, A56, INTEGRA1:def 4;

then A60: divset (D,k) = [.(D . (k - 1)),(D . k).] by INTEGRA1:4;

1 < k by A51, A59, A56, XXREAL_0:1;

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;then A60: divset (D,k) = [.(D . (k - 1)),(D . k).] by INTEGRA1:4;

1 < k by A51, A59, A56, XXREAL_0:1;

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

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 A52, A4, INTEGRA1:def 4;

then A62: divset (D,k) = [.(D . (k - 1)),(D . k).] by INTEGRA1:4;

len D = len F by A4, FINSEQ_3:29;

then A63: ( 1 < k & k < len D ) by A51, A61, XXREAL_0:1;

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 A62, XXREAL_1:24; :: thesis: verum

end;then A62: divset (D,k) = [.(D . (k - 1)),(D . k).] by INTEGRA1:4;

len D = len F by A4, FINSEQ_3:29;

then A63: ( 1 < k & k < len D ) by A51, A61, XXREAL_0:1;

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 A62, XXREAL_1:24; :: thesis: verum

divset (D,k) c= A by A52, A4, INTEGRA1:8;

then A65: divset (D,k) c= dom f by A2;

A66: rng f is bounded_above by A1, SEQ_2:def 8, INTEGRA1:13;

f = f | (dom f) ;

then f | (divset (D,k)) is bounded by A1, A65, RFUNCT_1:74;

then A67: rng (f | (divset (D,k))) is real-bounded by INTEGRA1:15;

(f | (divset (D,k))) . x = f . x by A51, A53, FUNCT_1:49;

then f . x in rng (f | (divset (D,k))) by A64, FUNCT_1:3;

hence ( upper_bound (rng f) >= g . x & g . x >= f . x ) by A66, A51, A67, SEQ_4:def 1, SEQ_4:48, RELAT_1:70; :: thesis: verum