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 = lower_bound (rng (f | (divset (D,k)))) ) by A3, Th10;
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 = lower_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 A11: B-Meas . A = b1 - a1 by A3, MEASURE5:6;
then A12: B-Meas . A1 < +infty by XXREAL_0:4;
defpred S₁[ 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 S₁[k,r]

proof

let k be Nat; :: thesis:
assume k in Seg (len F) ; :: thesis:
reconsider r = lower_bound (rng (f | (divset (D,k)))) as Element of ExtREAL by XXREAL_0:def 1;
take r ; :: thesis:
thus S₁[k,r] ; :: thesis:

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
S₁[k,h . k] ) ) from FINSEQ_1:sch 5(A13);
A15: dom h = dom F by A14, FINSEQ_1:def 3;
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:
assume A17: k in dom F ; :: thesis:
then A18: F . k in rng F by FUNCT_1:3;
let x be object ; :: thesis:
assume A19: x in F . k ; :: thesis:
then x in dom g by A5, A8, A18, TARSKI:def 4;
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 A19, A20, PROB_2:def 2, XBOOLE_0:3;
hence g . x = h . k by A14, A17, A15, A20; :: thesis:

end;

defpred S₂[ Nat, ExtReal] means ( $2 = (h . $1) * ((B-Meas * F) . $1) & $2 is Real );
A21: 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 A22: k in Seg (len F) ; :: thesis:
then A23: ( h . k = lower_bound (rng (f | (divset (D,k)))) & h . k is Real ) by A14;
A24: F . k c= A by A5, A22, A14, A15, FUNCT_1:3, ZFMISC_1:74;
F . k in Borel_Sets by A22, A14, A15, PARTFUN1:4;
then ( 0 <= B-Meas . (F . k) & B-Meas . (F . k) <= B-Meas . A1 ) by A24, SUPINF_2:51, MEASURE1:31;
then ( 0 <= B-Meas . (F . k) & B-Meas . (F . k) < +infty ) by A11, XXREAL_0:2, XXREAL_0:4;
then ( 0 <= (B-Meas * F) . k & (B-Meas * F) . k < +infty ) by A22, A14, A15, FUNCT_1:13;
then A25: (B-Meas * F) . k in REAL by XXREAL_0:14;
reconsider r = (h . k) * ((B-Meas * F) . k) as Element of ExtREAL ;
thus ex r being Element of ExtREAL st S₂[k,r] by A25, A23; :: thesis:

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
S₂[k,z . k] ) ) from FINSEQ_1:sch 5(A21);
A27: dom z = dom F by A26, FINSEQ_1:def 3;
A28: for k being Nat st k in dom z holds
z . k = (h . k) * ((B-Meas * F) . k) by A26;
A29: Integral (B-Meas,g) = Sum z by A7, A8, A12, A16, A27, A28, Th18, A5, A15, MESFUNC3:def 1;
len (lower_volume (f,D)) = len D by INTEGRA1:def 7;
then A30: dom z = dom (lower_volume (f,D)) by A27, A4, FINSEQ_3:29;
A31: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A32: ( lower_bound A = a & upper_bound A = b ) by A3, INTEGRA1:5;
for p being object st p in dom z holds
z . p = (lower_volume (f,D)) . p

proof

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

proof

per cases ;

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

then F . p1 = [.a,b.] by A33, A27, A6;
then B-Meas . (F . p1) = b - a by A3, Th5;
then A36: (B-Meas * F) . p1 = b - a by A33, A27, FUNCT_1:13;
( 1 <= p1 & p1 <= 1 ) by A33, A27, A4, A35, 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 A33, A27, A4, A35, INTEGRA1:def 4;
then ( lower_bound (divset (D,p1)) = a & upper_bound (divset (D,p1)) = b ) by A32, INTEGRA1:def 2;
hence (B-Meas * F) . p1 = vol (divset (D,p1)) by A36, INTEGRA1:def 5; :: thesis:

end;

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

( D . p1 in rng D & rng D c= A ) by A33, A27, A4, FUNCT_1:3, INTEGRA1:def 2;
then A38: ( a <= D . p1 & D . p1 <= b ) by A3, XXREAL_1:1;

per cases ;

suppose A39: p1 = 1 ; :: thesis:

then F . p1 = [.a,(D . 1).[ by A6, A33, A27, A37;
then B-Meas . (F . p1) = (D . 1) - a by A38, A39, Th5;
then A40: (B-Meas * F) . p1 = (D . 1) - a by A33, A27, FUNCT_1:13;
( lower_bound (divset (D,p1)) = lower_bound A & upper_bound (divset (D,p1)) = D . 1 ) by A33, A27, A4, A39, INTEGRA1:def 4;
hence (B-Meas * F) . p1 = vol (divset (D,p1)) by A40, A32, INTEGRA1:def 5; :: thesis:

end;

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

len D >= 1 by FINSEQ_1:20;
then len D > 1 by A37, XXREAL_0:1;
then A42: p1 -' 1 >= 1 by A41, NAT_D:49;
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 A42, A41, A43, FINSEQ_3:25, XREAL_1:43;
then D . (p1 - 1) <= D . p1 by A43, A33, A27, A4, VALUED_0:def 15, XREAL_1:43;
then B-Meas . (F . p1) = (D . p1) - (D . (p1 - 1)) by A44, Th5;
then A45: (B-Meas * F) . p1 = (D . p1) - (D . (p1 - 1)) by A33, A27, FUNCT_1:13;
( lower_bound (divset (D,p1)) = D . (p1 - 1) & upper_bound (divset (D,p1)) = D . p1 ) by A33, A27, A4, A41, A37, INTEGRA1:def 4;
hence (B-Meas * F) . p1 = vol (divset (D,p1)) by A45, INTEGRA1:def 5; :: thesis:

end;

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

( 1 <= p1 & p1 <= len D ) by A33, A27, A4, FINSEQ_3:25;
then A47: ( 1 < p1 & p1 < len D ) by A46, XXREAL_0:1;
then A48: F . p1 = [.(D . (p1 -' 1)),(D . p1).[ by A6, A33, A27;
A49: 1 <= p1 -' 1 by A47, NAT_D:49;
then A50: p1 -' 1 = p1 - 1 by NAT_D:39;
p1 - 1 <= p1 by XREAL_1:43;
then p1 -' 1 < len D by A47, A50, XXREAL_0:2;
then p1 -' 1 in dom D by A49, FINSEQ_3:25;
then D . (p1 -' 1) <= D . p1 by A50, A33, A27, A4, VALUED_0:def 15, XREAL_1:43;
then B-Meas . (F . p1) = (D . p1) - (D . (p1 - 1)) by A48, A50, Th5;
then A51: (B-Meas * F) . p1 = (D . p1) - (D . (p1 - 1)) by A33, A27, FUNCT_1:13;
( lower_bound (divset (D,p1)) = D . (p1 - 1) & upper_bound (divset (D,p1)) = D . p1 ) by A33, A27, A4, A46, INTEGRA1:def 4;
hence (B-Meas * F) . p1 = vol (divset (D,p1)) by A51, INTEGRA1:def 5; :: thesis:

end;

A52: h . p1 = lower_bound (rng (f | (divset (D,p1)))) by A33, A14, A26;
z . p = (h . p1) * ((B-Meas * F) . p1) by A26, A33;
then z . p = (lower_bound (rng (f | (divset (D,p1))))) * (vol (divset (D,p1))) by A34, A52, XXREAL_3:def 5;
hence z . p = (lower_volume (f,D)) . p by A33, A27, A4, INTEGRA1:def 7; :: thesis:

end;

then Sum z = Sum (lower_volume (f,D)) by A30, FUNCT_1:2, MESFUNC3:2;
hence Integral (B-Meas,g) = lower_sum (f,D) by A29, INTEGRA1:def 9; :: thesis:
thus for x being Real st x in A holds
( lower_bound (rng f) <= g . x & g . x <= f . x ) :: thesis:

proof

let x be Real; :: thesis:
assume A53: x in A ; :: thesis:
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 A54, FINSEQ_3:25;
A56: F . k c= divset (D,k)

proof

per cases ;

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

then A58: F . k = [.a,b.] by A6, A55;
len D = len F by A4, FINSEQ_3:29;
then k = 1 by A54, A57, XXREAL_0:1;
then ( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = D . 1 ) by A55, A4, INTEGRA1:def 4;
then ( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = upper_bound A ) by A57, INTEGRA1:def 2;
hence F . k c= divset (D,k) by A31, A58, A3, INTEGRA1:4; :: thesis:

end;

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

per cases ;

suppose A60: k = 1 ; :: thesis:

then ( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = D . k ) by A55, A4, INTEGRA1:def 4;
then A61: divset (D,k) = [.a,(D . k).] by A32, INTEGRA1:4;
F . k = [.a,(D . k).[ by A55, A59, A60, A6;
hence F . k c= divset (D,k) by A61, XXREAL_1:24; :: thesis:

end;

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

then ( lower_bound (divset (D,k)) = D . (k - 1) & upper_bound (divset (D,k)) = D . k ) by A55, A4, A59, INTEGRA1:def 4;
then A63: divset (D,k) = [.(D . (k - 1)),(D . k).] by INTEGRA1:4;
1 < k by A54, A62, A59, 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 A55, A59, A62, A6, A63; :: thesis:

end;

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

then ( lower_bound (divset (D,k)) = D . (k - 1) & upper_bound (divset (D,k)) = D . k ) by A55, A4, INTEGRA1:def 4;
then A65: divset (D,k) = [.(D . (k - 1)),(D . k).] by INTEGRA1:4;
len D = len F by A4, FINSEQ_3:29;
then A66: ( 1 < k & k < len D ) by A54, A64, 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 A55, A66, A6;
hence F . k c= divset (D,k) by A65, XXREAL_1:24; :: thesis:

end;

then A67: x in dom (f | (divset (D,k))) by A54, A2, A53, RELAT_1:57;
divset (D,k) c= A by A55, A4, INTEGRA1:8;
then A68: divset (D,k) c= dom f by A2;
A69: rng f is bounded_below by A1, SEQ_2:def 8, INTEGRA1:11;
f = f | (dom f) ;
then f | (divset (D,k)) is bounded by A1, A68, RFUNCT_1:74;
then A70: rng (f | (divset (D,k))) is real-bounded by INTEGRA1:15;
(f | (divset (D,k))) . x = f . x by A54, A56, FUNCT_1:49;
then f . x in rng (f | (divset (D,k))) by A67, FUNCT_1:3;
hence ( lower_bound (rng f) <= g . x & g . x <= f . x ) by A69, A54, A70, RELAT_1:70, SEQ_4:def 2, SEQ_4:47; :: thesis:

end;