theorem :: INTEGR26:44

for f being 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) )