let A be 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 13; :: thesis:

end;

then reconsider k1 = (len D) - 1 as Element of NAT ;
deffunc H₁( Nat) -> Element of REAL = f . (lower_bound (divset D,($1 + 1)));
deffunc H₂( Nat) -> Element of REAL = (f . (upper_bound (divset D,$1))) - (f . (lower_bound (divset D,$1)));
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 7;
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

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 INTEGRA1:4;
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 6;
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:3;
then A22: i + 1 <= k1 + 1 by XREAL_1:9;
1 <= i by A21, FINSEQ_1:3;
then 1 + 0 <= i + 1 by XREAL_1:9;
then i + 1 in Seg (len D) by A22, FINSEQ_1:3;
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:7;
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

per cases ;

suppose A26: i = 1 ; :: thesis:

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

end;

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

i >= 1 by A21, FINSEQ_1:3;
then i + 1 >= 1 + 1 by XREAL_1:8;
then A28: i + 1 <> 1 ;
upper_bound (divset D,i) = D . i by A24, A27, INTEGRA1:def 5;
hence upper_bound (divset D,i) = lower_bound (divset D,(i + 1)) by A23, A25, A28, INTEGRA1:def 5; :: 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 bounded

proof

dom (f `| X) = X by A2, FDIFF_1:def 8;
then reconsider g = f `| X as PartFunc of X,REAL by RELSET_1:13;
let k be Element of NAT ; :: thesis:
assume k in dom D ; :: thesis:
consider r1 being real number such that
A31: for x being set st x in A /\ (dom (f `| X)) holds
(f `| X) . x <= r1 by A3, RFUNCT_1:87;
consider r2 being real number such that
A32: for x being set st x in A /\ (dom (f `| X)) holds
(f `| X) . x >= r2 by A3, RFUNCT_1:88;
A33: dom ((f `| X) | A) = (dom (f `| X)) /\ A by RELAT_1:90;
for x being set st x in A /\ (dom ((f `| X) || A)) holds
((f `| X) || A) . x >= r2

proof

let x be set ; :: 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:70; :: thesis:

end;

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

proof

let x be set ; :: 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:70; :: thesis:

end;

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

end;

deffunc H₃( Nat) -> Element of REAL = f . (upper_bound (divset D,$1));
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;
( 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 ^ <*(f . (upper_bound A))*>) holds
p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) ) )

proof

now

per cases by A46, NAT_2:31;

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:4, TARSKI:def 1;
s1 = {} by A39, A47;
then s1 ^ <*(f . (upper_bound A))*> = <*(f . (upper_bound A))*> by FINSEQ_1:47;
then A50: (s1 ^ <*(f . (upper_bound A))*>) /. 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:47;
then A52: (<*(f . (lower_bound A))*> ^ 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 5;
p . i = (f . (upper_bound (divset D,i))) - (f . (lower_bound (divset D,i))) by A4, A19, A47, A48;
hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) by A49, A51, A50, A52, A53, INTEGRA1:def 5; :: thesis:

end;

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

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

now

per cases ;

suppose A56: i = 1 ; :: thesis:

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

end;

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

then i - (len s1) in Seg 1 by A39, FINSEQ_1:4, 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 ^ <*(f . (upper_bound A))*>) /. i = f . (upper_bound A) by A39, A44, A64, FINSEQ_1:def 8;
A67: i - (len <*(f . (lower_bound A))*>) = i - 1 by FINSEQ_1:57;
A68: i <> 1 by A54, A64;
i in Seg (len D) by A64, FINSEQ_1:5;
then A69: i in dom D by FINSEQ_1:def 3;
p . i = (f . (upper_bound (divset D,i))) - (f . (lower_bound (divset D,i))) by A4, A19, A64, FINSEQ_1:5;
then p . i = (f . (upper_bound (divset D,i))) - (f . (D . (i - 1))) by A69, A68, INTEGRA1:def 5;
then A70: p . i = (f . (D . i)) - (f . (D . (i - 1))) by A69, A68, INTEGRA1:def 5;
i - 1 <> 0 by A54, A64;
then i - 1 in Seg k1 by A64, FINSEQ_1:5;
then A71: ( (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;
then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . (i - (len <*(f . (lower_bound A))*>)) by FINSEQ_1:def 7;
then (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound (divset D,i)) by A29, A67, A71;
then (<*(f . (lower_bound A))*> ^ s2) . i = f . (D . (i - 1)) by A69, A68, INTEGRA1:def 5;
hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) by A45, A64, A66, A70, INTEGRA1:def 2; :: thesis:

end;

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

(len s1) + (len <*(f . (upper_bound A))*>) = k1 + 1 by A39, FINSEQ_1:56;
then A73: i in Seg (len D) by A43, FINSEQ_1:def 7;
A74: ( 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 A73, FINSEQ_1:3;
then not i is trivial by A72, NAT_2:def 1;
then i >= 1 + 1 by NAT_2:31;
then A75: i - 1 >= 1 by XREAL_1:21;
A76: 1 <= i by A73, FINSEQ_1:3;
i <= len D by A73, FINSEQ_1:3;
then A77: i < k1 + 1 by A72, XXREAL_0:1;
then A78: i <= k1 by NAT_1:13;
then i in Seg (len s1) by A39, A76, FINSEQ_1:3;
hence i in dom s1 by FINSEQ_1:def 3; :: thesis:
thus i in Seg k1 by A76, A78, FINSEQ_1:3; :: thesis:
i <= k1 by A77, NAT_1:13;
then i - 1 <= k1 - 1 by XREAL_1:11;
then A79: (i - 1) + 0 <= (k1 - 1) + 1 by XREAL_1:9;
ex j being Nat st i = 1 + j by A76, NAT_1:10;
hence i - 1 in Seg k1 by A75, A79, FINSEQ_1:3; :: thesis:
then A80: i - (len <*(f . (lower_bound A))*>) in Seg (len s2) by A29, FINSEQ_1:56;
thus (i - 1) + 1 = i ; :: thesis:
thus i - (len <*(f . (lower_bound A))*>) in dom s2 by A80, FINSEQ_1:def 3; :: thesis:

end;

end;

hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) ; :: thesis:

end;

hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) ; :: thesis:

end;

then Sum p = (Sum (s1 ^ <*(f . (upper_bound A))*>)) - (Sum (<*(f . (lower_bound A))*> ^ s2)) by INTEGRA1:24;
then Sum p = ((Sum s1) + (f . (upper_bound A))) - (Sum (<*(f . (lower_bound A))*> ^ s2)) by RVSUM_1:104;
then A84: Sum p = ((Sum s1) + (f . (upper_bound A))) - ((f . (lower_bound A)) + (Sum s2)) by RVSUM_1:106;
A85: dom s1 = Seg k1 by A39, FINSEQ_1:def 3;
A86: 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 A87: i in dom s1 ; :: thesis:
then s1 . i = f . (upper_bound (divset D,i)) by A39;
then s1 . i = f . (lower_bound (divset D,(i + 1))) by A20, A85, A87;
hence s1 . i = s2 . i by A86, A29, A40, A87; :: thesis:

end;

then A88: s1 = s2 by A39, A29, FINSEQ_2:10;
A89: 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

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

end;

A96: 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:
A97: vol (divset D,k) >= 0 by INTEGRA1:11;
assume A98: k in dom D ; :: thesis:
then consider r being Real such that
A99: r in divset D,k and
A100: (f . (upper_bound (divset D,k))) - (f . (lower_bound (divset D,k))) = (diff f,r) * (vol (divset D,k)) by A6;
A101: rng (((f `| X) || A) | (divset D,k)) is bounded by A30, A98;
diff f,r in rng (((f `| X) || A) | (divset D,k)) by A89, A98, A99;
then diff f,r <= upper_bound (rng (((f `| X) || A) | (divset D,k))) by A101, SEQ_4:def 4;
then (diff f,r) * (vol (divset D,k)) <= (upper_bound (rng (((f `| X) || A) | (divset D,k)))) * (vol (divset D,k)) by A97, XREAL_1:66;
hence (f . (upper_bound (divset D,k))) - (f . (lower_bound (divset D,k))) <= (upper_volume ((f `| X) || A),D) . k by A98, A100, INTEGRA1:def 7; :: thesis:

end;

A102: (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 7;
then reconsider q = upper_volume ((f `| X) || A),D as Element of (len D) -tuples_on REAL by FINSEQ_2:110;
A103: 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 k in Seg (len D) ; :: thesis:
then ( (f . (upper_bound (divset D,k))) - (f . (lower_bound (divset D,k))) = p . k & k in dom D ) by A4, A19, FINSEQ_1:def 3;
hence p . k <= (upper_volume ((f `| X) || A),D) . k by A96; :: thesis:

end;

reconsider p = p as Element of (len D) -tuples_on REAL by A4, FINSEQ_2:110;
Sum p <= Sum q by A103, RVSUM_1:112;
hence (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum ((f `| X) || A),D by A88, A84, INTEGRA1:def 9; :: thesis:

end;

A104: 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 A105: k in dom D ; :: thesis:
then A106: ( 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:11, INTEGRA1:def 8;
A107: rng (((f `| X) || A) | (divset D,k)) is bounded by A30, A105;
consider r being Real such that
A108: r in divset D,k and
A109: (f . (upper_bound (divset D,k))) - (f . (lower_bound (divset D,k))) = (diff f,r) * (vol (divset D,k)) by A6, A105;
diff f,r in rng (((f `| X) || A) | (divset D,k)) by A89, A105, A108;
then diff f,r >= lower_bound (rng (((f `| X) || A) | (divset D,k))) by A107, SEQ_4:def 5;
hence (f . (upper_bound (divset D,k))) - (f . (lower_bound (divset D,k))) >= (lower_volume ((f `| X) || A),D) . k by A109, A106, XREAL_1:66; :: 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 8;
then reconsider q = lower_volume ((f `| X) || A),D as Element of (len D) -tuples_on REAL by FINSEQ_2:110;
A110: 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 k in Seg (len D) ; :: thesis:
then ( (f . (upper_bound (divset D,k))) - (f . (lower_bound (divset D,k))) = p . k & k in dom D ) by A4, A19, FINSEQ_1:def 3;
hence p . k >= (lower_volume ((f `| X) || A),D) . k by A104; :: thesis:

end;

reconsider p = p as Element of (len D) -tuples_on REAL by A4, FINSEQ_2:110;
Sum q <= Sum p by A110, RVSUM_1:112;
hence (f . (upper_bound A)) - (f . (lower_bound A)) >= lower_sum ((f `| X) || A),D by A88, A84, INTEGRA1:def 10; :: 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 A102; :: thesis: