theorem Th43: :: INTEGR26:43

for a, b being Real
for f being PartFunc of REAL,REAL
for D being Division of ['a,b'] st a < b & f is_differentiable_on_interval ['a,b'] & f `\ ['a,b'] is bounded holds
( lower_sum (((f `\ ['a,b']) || ['a,b']),D) <= (f . b) - (f . a) & (f . b) - (f . a) <= upper_sum (((f `\ ['a,b']) || ['a,b']),D) )