let f be PartFunc of REAL,REAL; for a, b being Real
for I being non empty Interval st a in I & b in I & a < b & f is_differentiable_on_interval I & f `\ I is_integrable_on ['a,b'] & f `\ I is bounded holds
( integral ((f `\ ['a,b']),a,b) = (f . b) - (f . a) & integral ((f `\ I),a,b) = (f . b) - (f . a) )
let a, b be Real; for I being non empty Interval st a in I & b in I & a < b & f is_differentiable_on_interval I & f `\ I is_integrable_on ['a,b'] & f `\ I is bounded holds
( integral ((f `\ ['a,b']),a,b) = (f . b) - (f . a) & integral ((f `\ I),a,b) = (f . b) - (f . a) )
let I be non empty Interval; ( a in I & b in I & a < b & f is_differentiable_on_interval I & f `\ I is_integrable_on ['a,b'] & f `\ I is bounded implies ( integral ((f `\ ['a,b']),a,b) = (f . b) - (f . a) & integral ((f `\ I),a,b) = (f . b) - (f . a) ) )
assume that
A1:
( a in I & b in I )
and
A2:
a < b
and
A3:
f is_differentiable_on_interval I
and
A4:
f `\ I is_integrable_on ['a,b']
and
A5:
f `\ I is bounded
; ( integral ((f `\ ['a,b']),a,b) = (f . b) - (f . a) & integral ((f `\ I),a,b) = (f . b) - (f . a) )
reconsider J = ['a,b'] as non empty closed_interval Subset of REAL ;
A6:
J = [.a,b.]
by A2, INTEGRA5:def 3;
then A7:
['a,b'] c= I
by A1, Th3;
A8:
( a = inf J & b = sup J )
by A2, A6, MEASURE6:10, MEASURE6:14;
then A9:
f is_differentiable_on_interval J
by A3, A7, A2, FDIFF_12:38;
(f `\ I) | J is_integrable_on J
by A4;
then A10:
f `\ J is_integrable_on J
by A3, A6, A1, Th3, A2, A8, Th17;
(f `\ I) | J is bounded
by A5;
then
f `\ J is bounded
by A3, A6, A1, Th3, A2, A8, Th17;
then A11:
integral ((f `\ ['a,b']),['a,b']) = (f . b) - (f . a)
by A2, A9, A10, Lm4;
hence
integral ((f `\ ['a,b']),a,b) = (f . b) - (f . a)
by A2, INTEGRA5:def 4; integral ((f `\ I),a,b) = (f . b) - (f . a)
integral ((f `\ I),a,b) = integral ((f `\ I),J)
by A2, INTEGRA5:def 4;
then
integral ((f `\ I),a,b) = integral (((f `\ I) | J) || J)
;
hence
integral ((f `\ I),a,b) = (f . b) - (f . a)
by A11, A3, A6, A1, A2, A8, Th3, Th17; verum