let A be non empty closed_interval Subset of REAL; :: thesis:
let X be set ; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
let D be Division of A; :: thesis:
assume that
A1: A c= X and
A2: f is_differentiable_on X and
A3: (f `| X) | A is bounded ; :: thesis:
(len D) - 1 in NAT

proof

ex j being Nat st len D = 1 + j by NAT_1:10, NAT_1:14;
hence (len D) - 1 in NAT by ORDINAL1:def 12; :: thesis:

end;

then reconsider k1 = (len D) - 1 as Element of NAT ;
deffunc H₁( Nat) -> Element of REAL = In ((f . (lower_bound (divset (D,($1 + 1))))),REAL);
deffunc H₂( Nat) -> Element of REAL = In (((f . (upper_bound (divset (D,$1)))) - (f . (lower_bound (divset (D,$1))))),REAL);
consider p being FinSequence of REAL such that
A4: ( len p = len D & ( for i being Nat st i in dom p holds
p . i = H₂(i) ) ) from FINSEQ_2:sch 1();
X c= dom f by A2, FDIFF_1:def 6;
then A5: A c= dom f by A1, XBOOLE_1:1;
A6: for k being Element of NAT st k in dom D holds
ex r being Real st
( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )

proof

let k be Element of NAT ; :: thesis:
assume A7: k in dom D ; :: thesis:

now :: thesis:

per cases ;

suppose A8: lower_bound (divset (D,k)) = upper_bound (divset (D,k)) ; :: thesis:

consider r being Real such that
A9: r = upper_bound (divset (D,k)) ;
A10: r in divset (D,k)

proof

ex a, b being Real st
( a <= b & a = lower_bound (divset (D,k)) & b = upper_bound (divset (D,k)) ) by SEQ_4:11;
hence r in divset (D,k) by A9, INTEGRA2:1; :: thesis:

end;

(upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = 0 by A8;
then vol (divset (D,k)) = 0 by INTEGRA1:def 5;
then (diff (f,r)) * (vol (divset (D,k))) = 0 ;
hence ex r being Real st
( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) by A8, A10; :: thesis:

end;

suppose A11: lower_bound (divset (D,k)) <> upper_bound (divset (D,k)) ; :: thesis:

end;

hence ex r being Real st
( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) ; :: thesis:

end;

A19: dom p = Seg (len D) by A4, FINSEQ_1:def 3;
A20: for i being Element of NAT st i in Seg k1 holds
upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))

proof

let i be Element of NAT ; :: thesis:
assume A21: i in Seg k1 ; :: thesis:
then i <= k1 by FINSEQ_1:1;
then A22: i + 1 <= k1 + 1 by XREAL_1:7;
1 <= i by A21, FINSEQ_1:1;
then 1 + 0 <= i + 1 by XREAL_1:7;
then i + 1 in Seg (len D) by A22, FINSEQ_1:1;
then A23: i + 1 in dom D by FINSEQ_1:def 3;
k1 + 1 = len D ;
then k1 <= len D by NAT_1:11;
then Seg k1 c= Seg (len D) by FINSEQ_1:5;
then i in Seg (len D) by A21;
then A24: i in dom D by FINSEQ_1:def 3;
A25: (i + 1) - 1 = i ;

now :: thesis:

per cases ;

suppose A26: i = 1 ; :: thesis:

then upper_bound (divset (D,i)) = D . i by A24, INTEGRA1:def 4;
hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) by A23, A25, A26, INTEGRA1:def 4; :: thesis:

end;

suppose A27: i <> 1 ; :: thesis:

i >= 1 by A21, FINSEQ_1:1;
then i + 1 >= 1 + 1 by XREAL_1:6;
then A28: i + 1 <> 1 ;
upper_bound (divset (D,i)) = D . i by A24, A27, INTEGRA1:def 4;
hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) by A23, A25, A28, INTEGRA1:def 4; :: thesis:

end;

hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) ; :: thesis:

end;

consider s2 being FinSequence of REAL such that
A29: ( len s2 = k1 & ( for i being Nat st i in dom s2 holds
s2 . i = H₁(i) ) ) from FINSEQ_2:sch 1();
A30: for k being Element of NAT st k in dom D holds
rng (((f `| X) || A) | (divset (D,k))) is real-bounded

proof

dom (f `| X) = X by A2, FDIFF_1:def 7;
then reconsider g = f `| X as PartFunc of X,REAL by RELSET_1:5;
let k be Element of NAT ; :: thesis:
assume k in dom D ; :: thesis:
consider r1 being Real such that
A31: for x being object st x in A /\ (dom (f `| X)) holds
(f `| X) . x <= r1 by A3, RFUNCT_1:70;
consider r2 being Real such that
A32: for x being object st x in A /\ (dom (f `| X)) holds
(f `| X) . x >= r2 by A3, RFUNCT_1:71;
A33: dom ((f `| X) | A) = (dom (f `| X)) /\ A by RELAT_1:61;
for x being object st x in A /\ (dom ((f `| X) || A)) holds
((f `| X) || A) . x >= r2

proof

let x be object ; :: thesis:
A34: A /\ (A /\ (dom (f `| X))) = (A /\ A) /\ (dom (f `| X)) by XBOOLE_1:16
.= A /\ (dom (f `| X)) ;
reconsider y = g . x as Real ;
assume A35: x in A /\ (dom ((f `| X) || A)) ; :: thesis:
then y >= r2 by A32, A33, A34;
hence ((f `| X) || A) . x >= r2 by A33, A35, A34, FUNCT_1:47; :: thesis:

end;

then ((f `| X) || A) | A is bounded_below by RFUNCT_1:71;
then A36: rng (((f `| X) || A) | (divset (D,k))) is bounded_below by INTEGRA4:19;
for x being object st x in A /\ (dom ((f `| X) || A)) holds
((f `| X) || A) . x <= r1

proof

let x be object ; :: thesis:
A37: A /\ (A /\ (dom (f `| X))) = (A /\ A) /\ (dom (f `| X)) by XBOOLE_1:16
.= A /\ (dom (f `| X)) ;
reconsider y = g . x as Real ;
assume A38: x in A /\ (dom ((f `| X) || A)) ; :: thesis:
then y <= r1 by A31, A33, A37;
hence ((f `| X) || A) . x <= r1 by A33, A38, A37, FUNCT_1:47; :: thesis:

end;

then ((f `| X) || A) | A is bounded_above by RFUNCT_1:70;
then rng (((f `| X) || A) | (divset (D,k))) is bounded_above by INTEGRA4:18;
hence rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A36; :: thesis:

end;

deffunc H₃( Nat) -> Element of REAL = In ((f . (upper_bound (divset (D,$1)))),REAL);
consider s1 being FinSequence of REAL such that
A39: ( len s1 = k1 & ( for i being Nat st i in dom s1 holds
s1 . i = H₃(i) ) ) from FINSEQ_2:sch 1();
A40: dom s2 = Seg k1 by A29, FINSEQ_1:def 3;
reconsider flb = f . (lower_bound A), fub = f . (upper_bound A) as Element of REAL by XREAL_0:def 1;
( len (s1 ^ <*(f . (upper_bound A))*>) = len (<*(f . (lower_bound A))*> ^ s2) & len (s1 ^ <*(f . (upper_bound A))*>) = len p & ( for i being Element of NAT st i in dom (s1 ^ <*fub*>) holds
p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) ) )

proof

dom <*(f . (upper_bound A))*> = Seg 1 by FINSEQ_1:def 8;
then len <*(f . (upper_bound A))*> = 1 by FINSEQ_1:def 3;
then A41: len (s1 ^ <*(f . (upper_bound A))*>) = k1 + 1 by A39, FINSEQ_1:22;
dom <*(f . (lower_bound A))*> = Seg 1 by FINSEQ_1:def 8;
then len <*(f . (lower_bound A))*> = 1 by FINSEQ_1:def 3;
hence A42: len (s1 ^ <*(f . (upper_bound A))*>) = len (<*(f . (lower_bound A))*> ^ s2) by A29, A41, FINSEQ_1:22; :: thesis:
thus len (s1 ^ <*(f . (upper_bound A))*>) = len p by A4, A41; :: thesis:
let i be Element of NAT ; :: thesis:
assume A43: i in dom (s1 ^ <*fub*>) ; :: thesis:
then A44: (s1 ^ <*fub*>) /. i = (s1 ^ <*(f . (upper_bound A))*>) . i by PARTFUN1:def 6;
i in Seg (len (s1 ^ <*(f . (upper_bound A))*>)) by A43, FINSEQ_1:def 3;
then i in dom (<*(f . (lower_bound A))*> ^ s2) by A42, FINSEQ_1:def 3;
then A45: (<*flb*> ^ s2) /. i = (<*flb*> ^ s2) . i by PARTFUN1:def 6;
A46: ( len D = 1 or not len D is trivial ) by NAT_2:def 1;

now :: thesis:

per cases by A46, NAT_2:29;

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

then A48: i in Seg 1 by A41, A43, FINSEQ_1:def 3;
then A49: i = 1 by FINSEQ_1:2, TARSKI:def 1;
s1 = {} by A39, A47;
then s1 ^ <*(f . (upper_bound A))*> = <*(f . (upper_bound A))*> by FINSEQ_1:34;
then A50: (s1 ^ <*fub*>) /. i = f . (upper_bound A) by A44, A49, FINSEQ_1:def 8;
A51: i in dom D by A47, A48, FINSEQ_1:def 3;
s2 = {} by A29, A47;
then <*(f . (lower_bound A))*> ^ s2 = <*(f . (lower_bound A))*> by FINSEQ_1:34;
then A52: (<*flb*> ^ s2) /. i = f . (lower_bound A) by A45, A49, FINSEQ_1:def 8;
D . i = upper_bound A by A47, A49, INTEGRA1:def 2;
then A53: upper_bound (divset (D,i)) = upper_bound A by A49, A51, INTEGRA1:def 4;
p . i = H₂(i) by A4, A19, A47, A48
.= (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) ;
hence p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) by A49, A51, A50, A52, A53, INTEGRA1:def 4; :: thesis:

end;

suppose A54: len D >= 2 ; :: thesis:

1 = 2 - 1 ;
then A55: k1 >= 1 by A54, XREAL_1:9;

now :: thesis:

per cases ;

suppose A56: i = 1 ; :: thesis:

then A57: i in Seg 1 by FINSEQ_1:2, TARSKI:def 1;
then i in dom <*(f . (lower_bound A))*> by FINSEQ_1:def 8;
then (<*(f . (lower_bound A))*> ^ s2) . i = <*(f . (lower_bound A))*> . i by FINSEQ_1:def 7;
then A58: (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound A) by A56, FINSEQ_1:def 8;
Seg 1 c= Seg k1 by A55, FINSEQ_1:5;
then i in Seg k1 by A57;
then A59: i in dom s1 by A39, FINSEQ_1:def 3;
then (s1 ^ <*(f . (upper_bound A))*>) . i = s1 . i by FINSEQ_1:def 7
.= H₃(i) by A39, A59 ;
then A60: (s1 ^ <*(f . (upper_bound A))*>) . i = f . (upper_bound (divset (D,i))) ;
A61: i in Seg 2 by A56, FINSEQ_1:2, TARSKI:def 2;
A62: Seg 2 c= Seg (len D) by A54, FINSEQ_1:5;
then i in Seg (len D) by A61;
then A63: i in dom D by FINSEQ_1:def 3;
p . i = H₂(i) by A4, A19, A62, A61
.= (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) ;
hence p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) by A44, A45, A56, A63, A60, A58, INTEGRA1:def 4; :: thesis:

end;

suppose A64: i = len D ; :: thesis:

then i - (len s1) in Seg 1 by A39, FINSEQ_1:2, TARSKI:def 1;
then A65: i - (len s1) in dom <*(f . (upper_bound A))*> by FINSEQ_1:def 8;
i = (i - (len s1)) + (len s1) ;
then (s1 ^ <*(f . (upper_bound A))*>) . i = <*(f . (upper_bound A))*> . (i - (len s1)) by A65, FINSEQ_1:def 7;
then A66: (s1 ^ <*fub*>) /. i = f . (upper_bound A) by A39, A44, A64, FINSEQ_1:def 8;
A67: len <*(f . (lower_bound A))*> = 1 by FINSEQ_1:40;
A68: i <> 1 by A54, A64;
i in Seg (len D) by A64, FINSEQ_1:3;
then A69: i in dom D by FINSEQ_1:def 3;
p . i = H₂(i) by A4, A19, A64, FINSEQ_1:3
.= (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) ;
then p . i = (f . (upper_bound (divset (D,i)))) - (f . (D . (i - 1))) by A69, A68, INTEGRA1:def 4;
then A70: p . i = (f . (D . i)) - (f . (D . (i - 1))) by A69, A68, INTEGRA1:def 4;
i - 1 <> 0 by A54, A64;
then A71: i - 1 in Seg k1 by A64, FINSEQ_1:3;
then reconsider i1 = i - 1 as Nat ;
A72: ( (len <*(f . (lower_bound A))*>) + (i - (len <*(f . (lower_bound A))*>)) = i & i - (len <*(f . (lower_bound A))*>) in dom s2 ) by A29, A67, FINSEQ_1:def 3, A71;
then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . i1 by FINSEQ_1:def 7, A67
.= H₁(i1) by A29, A67, A72 ;
then (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound (divset (D,i))) ;
then (<*(f . (lower_bound A))*> ^ s2) . i = f . (D . (i - 1)) by A69, A68, INTEGRA1:def 4;
hence p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) by A45, A64, A66, A70, INTEGRA1:def 2; :: thesis:

end;

suppose A73: ( i <> 1 & i <> len D ) ; :: thesis:

(len s1) + (len <*(f . (upper_bound A))*>) = k1 + 1 by A39, FINSEQ_1:39;
then A74: i in Seg (len D) by A43, FINSEQ_1:def 7;
A75: ( i in dom s1 & i in Seg k1 & i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 )

proof

i <> 0 by A74, FINSEQ_1:1;
then not i is trivial by A73, NAT_2:def 1;
then i >= 1 + 1 by NAT_2:29;
then A76: i - 1 >= 1 by XREAL_1:19;
A77: 1 <= i by A74, FINSEQ_1:1;
i <= len D by A74, FINSEQ_1:1;
then A78: i < k1 + 1 by A73, XXREAL_0:1;
then A79: i <= k1 by NAT_1:13;
then i in Seg (len s1) by A39, A77, FINSEQ_1:1;
hence i in dom s1 by FINSEQ_1:def 3; :: thesis:
thus i in Seg k1 by A77, A79, FINSEQ_1:1; :: thesis:
i <= k1 by A78, NAT_1:13;
then i - 1 <= k1 - 1 by XREAL_1:9;
then A80: (i - 1) + 0 <= (k1 - 1) + 1 by XREAL_1:7;
ex j being Nat st i = 1 + j by A77, NAT_1:10;
hence i - 1 in Seg k1 by A76, A80, FINSEQ_1:1; :: thesis:
then A81: i - (len <*(f . (lower_bound A))*>) in Seg (len s2) by A29, FINSEQ_1:39;
thus (i - 1) + 1 = i ; :: thesis:
thus i - (len <*(f . (lower_bound A))*>) in dom s2 by A81, FINSEQ_1:def 3; :: thesis:

end;

end;

hence p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) ; :: thesis:

end;

hence p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) ; :: thesis:

end;

then Sum p = (Sum (s1 ^ <*(f . (upper_bound A))*>)) - (Sum (<*(f . (lower_bound A))*> ^ s2)) by INTEGRA1:22;
then Sum p = ((Sum s1) + (f . (upper_bound A))) - (Sum (<*(f . (lower_bound A))*> ^ s2)) by RVSUM_1:74;
then A86: Sum p = ((Sum s1) + (f . (upper_bound A))) - ((f . (lower_bound A)) + (Sum s2)) by RVSUM_1:76;
A87: dom s1 = Seg k1 by A39, FINSEQ_1:def 3;
A88: dom s1 = Seg k1 by A39, FINSEQ_1:def 3;
for i being Nat st i in dom s1 holds
s1 . i = s2 . i

proof

let i be Nat; :: thesis:
assume A89: i in dom s1 ; :: thesis:
then s1 . i = H₃(i) by A39
.= f . (upper_bound (divset (D,i))) ;
then s1 . i = f . (lower_bound (divset (D,(i + 1)))) by A20, A87, A89
.= H₁(i) ;
hence s1 . i = s2 . i by A88, A29, A40, A89; :: thesis:

end;

then A90: s1 = s2 by A39, A29, FINSEQ_2:9;
A91: for k being Element of NAT
for r being Real st k in dom D & r in divset (D,k) holds
diff (f,r) in rng (((f `| X) || A) | (divset (D,k)))

proof

A92: dom ((f `| X) | A) = (dom (f `| X)) /\ A by RELAT_1:61
.= X /\ A by A2, FDIFF_1:def 7
.= A by A1, XBOOLE_1:28 ;
let k be Element of NAT ; :: thesis:
let r be Real; :: thesis:
assume that
A93: k in dom D and
A94: r in divset (D,k) ; :: thesis:
A95: divset (D,k) c= A by A93, INTEGRA1:8;
then divset (D,k) c= X by A1, XBOOLE_1:1;
then (f `| X) . r = diff (f,r) by A2, A94, FDIFF_1:def 7;
then A96: diff (f,r) = ((f `| X) || A) . r by A94, A95, A92, FUNCT_1:47;
A97: dom (((f `| X) || A) | (divset (D,k))) = A /\ (divset (D,k)) by A92, RELAT_1:61
.= divset (D,k) by A93, INTEGRA1:8, XBOOLE_1:28 ;
then (((f `| X) || A) | (divset (D,k))) . r in rng (((f `| X) || A) | (divset (D,k))) by A94, FUNCT_1:def 3;
hence diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A94, A96, A97, FUNCT_1:47; :: thesis:

end;

A98: for k being Element of NAT st k in dom D holds
(f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k

proof

let k be Element of NAT ; :: thesis:
A99: vol (divset (D,k)) >= 0 by INTEGRA1:9;
assume A100: k in dom D ; :: thesis:
then consider r being Real such that
A101: r in divset (D,k) and
A102: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) by A6;
A103: rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A30, A100;
diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A91, A100, A101;
then diff (f,r) <= upper_bound (rng (((f `| X) || A) | (divset (D,k)))) by A103, SEQ_4:def 1;
then (diff (f,r)) * (vol (divset (D,k))) <= (upper_bound (rng (((f `| X) || A) | (divset (D,k))))) * (vol (divset (D,k))) by A99, XREAL_1:64;
hence (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k by A100, A102, INTEGRA1:def 6; :: thesis:

end;

A104: (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D)

proof

len (upper_volume (((f `| X) || A),D)) = len D by INTEGRA1:def 6;
then reconsider q = upper_volume (((f `| X) || A),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
A105: for k being Nat st k in Seg (len D) holds
p . k <= (upper_volume (((f `| X) || A),D)) . k

proof

let k be Nat; :: thesis:
assume A106: k in Seg (len D) ; :: thesis:
A107: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = H₂(k)
.= p . k by A4, A19, A106 ;
k in dom D by FINSEQ_1:def 3, A106;
hence p . k <= (upper_volume (((f `| X) || A),D)) . k by A98, A107; :: thesis:

end;

reconsider p = p as Element of (len D) -tuples_on REAL by A4, FINSEQ_2:92;
Sum p <= Sum q by A105, RVSUM_1:82;
hence (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) by A90, A86, INTEGRA1:def 8; :: thesis:

end;

A108: for k being Element of NAT st k in dom D holds
(f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k

proof

let k be Element of NAT ; :: thesis:
assume A109: k in dom D ; :: thesis:
then A110: ( vol (divset (D,k)) >= 0 & (lower_bound (rng (((f `| X) || A) | (divset (D,k))))) * (vol (divset (D,k))) = (lower_volume (((f `| X) || A),D)) . k ) by INTEGRA1:9, INTEGRA1:def 7;
A111: rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A30, A109;
consider r being Real such that
A112: r in divset (D,k) and
A113: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) by A6, A109;
diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A91, A109, A112;
then diff (f,r) >= lower_bound (rng (((f `| X) || A) | (divset (D,k)))) by A111, SEQ_4:def 2;
hence (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k by A113, A110, XREAL_1:64; :: thesis:

end;

(f . (upper_bound A)) - (f . (lower_bound A)) >= lower_sum (((f `| X) || A),D)

proof

len (lower_volume (((f `| X) || A),D)) = len D by INTEGRA1:def 7;
then reconsider q = lower_volume (((f `| X) || A),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
A114: for k being Nat st k in Seg (len D) holds
p . k >= (lower_volume (((f `| X) || A),D)) . k

proof

let k be Nat; :: thesis:
assume A115: k in Seg (len D) ; :: thesis:
A116: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = H₂(k)
.= p . k by A4, A19, A115 ;
k in dom D by FINSEQ_1:def 3, A115;
hence p . k >= (lower_volume (((f `| X) || A),D)) . k by A108, A116; :: thesis:

end;

reconsider p = p as Element of (len D) -tuples_on REAL by A4, FINSEQ_2:92;
Sum q <= Sum p by A114, RVSUM_1:82;
hence (f . (upper_bound A)) - (f . (lower_bound A)) >= lower_sum (((f `| X) || A),D) by A90, A86, INTEGRA1:def 9; :: thesis:

end;

hence ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) ) by A104; :: thesis: