let I be non empty closed_interval Subset of REAL; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
let D be Division of I; :: thesis:
assume that
A1: f is_differentiable_on_interval I and
A2: f `\ I is bounded ; :: thesis:
A3: f is_differentiable_on ].(inf I),(sup I).[ by A1, FDIFF_12:def 1;
reconsider k1 = (len D) - 1 as Element of NAT by ORDINAL1:def 12;
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();
A5: I c= dom f by A1, FDIFF_12:def 1;
A6: for k being 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)))) = ((f `\ I) . r) * (vol (divset (D,k))) )

proof

let k be 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;

((f `\ I) . r) * (vol (divset (D,k))) = 0 by A8;
hence ex r being Real st
( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = ((f `\ I) . 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)))) = ((f `\ I) . r) * (vol (divset (D,k))) ) ; :: thesis:

end;

A23: dom p = Seg (len D) by A4, FINSEQ_1:def 3;
A24: for i being Nat st i in Seg k1 holds
upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))

proof

let i be Nat; :: thesis:
assume A25: i in Seg k1 ; :: thesis:
then i <= k1 by FINSEQ_1:1;
then A26: i + 1 <= k1 + 1 by XREAL_1:7;
1 + 0 <= i + 1 by XREAL_1:7;
then i + 1 in Seg (len D) by A26, FINSEQ_1:1;
then A27: i + 1 in dom D by FINSEQ_1:def 3;
k1 + 1 = len D ;
then Seg k1 c= Seg (len D) by FINSEQ_1:5, NAT_1:11;
then i in Seg (len D) by A25;
then A28: i in dom D by FINSEQ_1:def 3;
A29: (i + 1) - 1 = i ;

now :: thesis:

per cases ;

suppose A30: i = 1 ; :: thesis:

then upper_bound (divset (D,i)) = D . i by A28, INTEGRA1:def 4;
hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) by A27, A29, A30, INTEGRA1:def 4; :: thesis:

end;

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

i >= 1 by A25, FINSEQ_1:1;
then i + 1 >= 1 + 1 by XREAL_1:6;
then A32: i + 1 <> 1 ;
upper_bound (divset (D,i)) = D . i by A28, A31, INTEGRA1:def 4;
hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) by A27, A29, A32, 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
A33: ( len s2 = k1 & ( for i being Nat st i in dom s2 holds
s2 . i = H₁(i) ) ) from FINSEQ_2:sch 1();
A34: for k being Nat st k in dom D holds
rng (((f `\ I) || I) | (divset (D,k))) is real-bounded

proof

A35: dom (f `\ I) = I by A1, FDIFF_12:def 2;
then reconsider g = f `\ I as PartFunc of I,REAL by RELSET_1:5;
let k be Nat; :: thesis:
assume k in dom D ; :: thesis:
A36: (f `\ I) | I = f `\ I by A35;
consider r1 being Real such that
A37: for x being object st x in I /\ (dom (f `\ I)) holds
(f `\ I) . x <= r1 by A2, A36, RFUNCT_1:70;
consider r2 being Real such that
A38: for x being object st x in I /\ (dom (f `\ I)) holds
(f `\ I) . x >= r2 by A2, A36, RFUNCT_1:71;
for x being object st x in I /\ (dom ((f `\ I) || I)) holds
((f `\ I) || I) . x >= r2

proof

let x be object ; :: thesis:
reconsider y = g . x as Real ;
assume x in I /\ (dom ((f `\ I) || I)) ; :: thesis:
then y >= r2 by A38;
hence ((f `\ I) || I) . x >= r2 ; :: thesis:

end;

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

proof

let x be object ; :: thesis:
reconsider y = g . x as Real ;
assume x in I /\ (dom ((f `\ I) || I)) ; :: thesis:
then y <= r1 by A37;
hence ((f `\ I) || I) . x <= r1 ; :: thesis:

end;

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

end;

deffunc H₃( Nat) -> Element of REAL = In ((f . (upper_bound (divset (D,$1)))),REAL);
consider s1 being FinSequence of REAL such that
A40: ( len s1 = k1 & ( for i being Nat st i in dom s1 holds
s1 . i = H₃(i) ) ) from FINSEQ_2:sch 1();
A41: dom s2 = Seg k1 by A33, FINSEQ_1:def 3;
reconsider flb = f . (lower_bound I), fub = f . (upper_bound I) as Element of REAL by XREAL_0:def 1;
( len (s1 ^ <*(f . (upper_bound I))*>) = len (<*(f . (lower_bound I))*> ^ s2) & len (s1 ^ <*(f . (upper_bound I))*>) = 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 I))*> = Seg 1 by FINSEQ_1:def 8;
then len <*(f . (upper_bound I))*> = 1 by FINSEQ_1:def 3;
then A42: len (s1 ^ <*(f . (upper_bound I))*>) = k1 + 1 by A40, FINSEQ_1:22;
dom <*(f . (lower_bound I))*> = Seg 1 by FINSEQ_1:def 8;
then len <*(f . (lower_bound I))*> = 1 by FINSEQ_1:def 3;
hence A43: len (s1 ^ <*(f . (upper_bound I))*>) = len (<*(f . (lower_bound I))*> ^ s2) by A33, A42, FINSEQ_1:22; :: thesis:
thus len (s1 ^ <*(f . (upper_bound I))*>) = len p by A4, A42; :: thesis:
let i be Element of NAT ; :: thesis:
assume A44: i in dom (s1 ^ <*fub*>) ; :: thesis:
then A45: (s1 ^ <*fub*>) /. i = (s1 ^ <*(f . (upper_bound I))*>) . i by PARTFUN1:def 6;
i in Seg (len (s1 ^ <*(f . (upper_bound I))*>)) by A44, FINSEQ_1:def 3;
then i in dom (<*(f . (lower_bound I))*> ^ s2) by A43, FINSEQ_1:def 3;
then A46: (<*flb*> ^ s2) /. i = (<*flb*> ^ s2) . i by PARTFUN1:def 6;
A47: ( len D = 1 or not len D is trivial ) by NAT_2:def 1;

now :: thesis:

per cases by A47, NAT_2:29;

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

then A49: i in Seg 1 by A42, A44, FINSEQ_1:def 3;
then A50: i = 1 by FINSEQ_1:2, TARSKI:def 1;
s1 = {} by A40, A48;
then s1 ^ <*(f . (upper_bound I))*> = <*(f . (upper_bound I))*> by FINSEQ_1:34;
then A51: (s1 ^ <*fub*>) /. i = f . (upper_bound I) by A45, A50;
A52: i in dom D by A48, A49, FINSEQ_1:def 3;
s2 = {} by A33, A48;
then <*(f . (lower_bound I))*> ^ s2 = <*(f . (lower_bound I))*> by FINSEQ_1:34;
then A53: (<*flb*> ^ s2) /. i = f . (lower_bound I) by A46, A50;
D . i = upper_bound I by A48, A50, INTEGRA1:def 2;
then A54: upper_bound (divset (D,i)) = upper_bound I by A50, A52, INTEGRA1:def 4;
p . i = H₂(i) by A4, A23, A48, A49;
hence p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) by A50, A52, A51, A53, A54, INTEGRA1:def 4; :: thesis:

end;

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

A56: 1 = 2 - 1 ;

now :: thesis:

per cases ;

suppose A57: i = 1 ; :: thesis:

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

end;

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

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

end;

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

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

proof

i <> 0 by A75, FINSEQ_1:1;
then not i is trivial by A74, NAT_2:def 1;
then i >= 1 + 1 by NAT_2:29;
then A77: i - 1 >= 1 by XREAL_1:19;
A78: 1 <= i by A75, FINSEQ_1:1;
i <= len D by A75, FINSEQ_1:1;
then A79: i < k1 + 1 by A74, XXREAL_0:1;
then A80: i <= k1 by NAT_1:13;
then i in Seg (len s1) by A40, A78, FINSEQ_1:1;
hence i in dom s1 by FINSEQ_1:def 3; :: thesis:
thus i in Seg k1 by A78, A80, FINSEQ_1:1; :: thesis:
i <= k1 by A79, NAT_1:13;
then i - 1 <= k1 - 1 by XREAL_1:9;
then (i - 1) + 0 <= (k1 - 1) + 1 by XREAL_1:7;
hence i - 1 in Seg k1 by A77, A78, FINSEQ_1:1; :: thesis:
then A81: i - (len <*(f . (lower_bound I))*>) in Seg (len s2) by A33, FINSEQ_1:39;
thus (i - 1) + 1 = i ; :: thesis:
thus i - (len <*(f . (lower_bound I))*>) 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 I))*>)) - (Sum (<*(f . (lower_bound I))*> ^ s2)) by INTEGRA1:22;
then Sum p = ((Sum s1) + (f . (upper_bound I))) - (Sum (<*(f . (lower_bound I))*> ^ s2)) by RVSUM_1:74;
then A86: Sum p = ((Sum s1) + (f . (upper_bound I))) - ((f . (lower_bound I)) + (Sum s2)) by RVSUM_1:76;
A87: dom s1 = Seg k1 by A40, 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 A88: i in dom s1 ; :: thesis:
then s1 . i = H₃(i) by A40;
then s1 . i = H₁(i) by A24, A87, A88;
hence s1 . i = s2 . i by A87, A33, A41, A88; :: thesis:

end;

then A89: s1 = s2 by A40, A33, FINSEQ_2:9;
A90: for k being Element of NAT
for r being Real st k in dom D & r in divset (D,k) holds
(f `\ I) . r in rng (((f `\ I) || I) | (divset (D,k)))

proof

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

end;

A97: 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 `\ I) || I),D)) . k

proof

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

end;

A103: (f . (upper_bound I)) - (f . (lower_bound I)) <= upper_sum (((f `\ I) || I),D)

proof

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

proof

let k be Nat; :: thesis:
assume A105: k in Seg (len D) ; :: thesis:
(f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = H₂(k) ;
then A106: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = p . k by A4, A23, A105;
k in dom D by FINSEQ_1:def 3, A105;
hence p . k <= (upper_volume (((f `\ I) || I),D)) . k by A97, A106; :: thesis:

end;

reconsider p = p as Element of (len D) -tuples_on REAL by A4, FINSEQ_2:92;
Sum p <= Sum q by A104, RVSUM_1:82;
hence (f . (upper_bound I)) - (f . (lower_bound I)) <= upper_sum (((f `\ I) || I),D) by A89, A86; :: thesis:

end;

A107: 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 `\ I) || I),D)) . k

proof

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

end;

(f . (upper_bound I)) - (f . (lower_bound I)) >= lower_sum (((f `\ I) || I),D)

proof

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

proof

let k be Nat; :: thesis:
assume A114: k in Seg (len D) ; :: thesis:
A115: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = H₂(k)
.= p . k by A4, A23, A114 ;
k in dom D by FINSEQ_1:def 3, A114;
hence p . k >= (lower_volume (((f `\ I) || I),D)) . k by A107, A115; :: thesis:

end;

reconsider p = p as Element of (len D) -tuples_on REAL by A4, FINSEQ_2:92;
Sum q <= Sum p by A113, RVSUM_1:82;
hence (f . (upper_bound I)) - (f . (lower_bound I)) >= lower_sum (((f `\ I) || I),D) by A89, A86; :: thesis:

end;

hence ( lower_sum (((f `\ I) || I),D) <= (f . (upper_bound I)) - (f . (lower_bound I)) & (f . (upper_bound I)) - (f . (lower_bound I)) <= upper_sum (((f `\ I) || I),D) ) by A103; :: thesis: