let A be non empty closed_interval Subset of REAL; :: thesis:
let f be PartFunc of A,REAL; :: thesis:
let D be Division of A; :: thesis:
assume that
A1: f is bounded and
A2: A c= dom f ; :: thesis:
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:
take g ; :: thesis:
thus dom F = dom D by A4; :: thesis:
thus union (rng F) = A by A5; :: thesis:
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:
thus g is_simple_func_in Borel_Sets by A7; :: thesis:
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:
thus dom g = A by A8; :: thesis:
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₁[ 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₁[k,r]

proof

let k be Nat; :: thesis:
assume k in Seg (len F) ; :: thesis:
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₁[k,r] ; :: thesis:

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
S₁[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

proof

let k be Nat; :: thesis:
assume A16: k in dom F ; :: thesis:
then A17: F . k in rng F by FUNCT_1:3;
let x be object ; :: thesis:
assume A18: x in F . k ; :: thesis:
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:

end;

defpred S₂[ 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₂[k,r]

proof

let k be Nat; :: thesis:
assume A21: k in Seg (len F) ; :: thesis:
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₂[k,r] by A22; :: thesis:

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
S₂[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

proof

let p be object ; :: thesis:
assume A30: p in dom z ; :: thesis:
then reconsider p1 = p as Nat ;
A31: (B-Meas * F) . p1 = vol (divset (D,p1))

proof

per cases ;

suppose A32: len D = 1 ; :: thesis:

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:

end;

suppose A34: len D <> 1 ; :: thesis:

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

per cases ;

suppose A36: p1 = 1 ; :: thesis:

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:

end;

suppose A38: p1 = len D ; :: thesis:

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:

end;

suppose A43: ( p1 <> 1 & p1 <> len D ) ; :: thesis:

( 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:

end;

A49: h . p1 = upper_bound (rng (f | (divset (D,p1)))) by A30, A13, A24;
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:

end;

then Sum z = Sum (upper_volume (f,D)) by A27, FUNCT_1:2, MESFUNC3:2;
hence Integral (B-Meas,g) = upper_sum (f,D) by A26, INTEGRA1:def 8; :: thesis:
thus for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) :: thesis:

proof

let x be Real; :: thesis:
assume A50: x in A ; :: thesis:
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

per cases ;

suppose A54: len D = 1 ; :: thesis:

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:

end;

suppose A56: len D <> 1 ; :: thesis:

per cases ;

suppose A57: k = 1 ; :: thesis:

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:

end;

suppose A59: k = len D ; :: thesis:

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:

end;

suppose A61: ( k <> 1 & k <> len D ) ; :: thesis:

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:

end;

then A64: x in dom (f | (divset (D,k))) by A51, A2, A50, RELAT_1:57;
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:

end;