let a, b be Real; :: thesis: 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) )
let f be PartFunc of REAL,REAL; :: thesis: 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) )
let D be Division of ['a,b']; :: thesis: ( a < b & f is_differentiable_on_interval ['a,b'] & f `\ ['a,b'] is bounded implies ( lower_sum (((f `\ ['a,b']) || ['a,b']),D) <= (f . b) - (f . a) & (f . b) - (f . a) <= upper_sum (((f `\ ['a,b']) || ['a,b']),D) ) )
assume that
A1: a < b and
A2: f is_differentiable_on_interval ['a,b'] and
A3: f `\ ['a,b'] is bounded ; :: thesis: ( lower_sum (((f `\ ['a,b']) || ['a,b']),D) <= (f . b) - (f . a) & (f . b) - (f . a) <= upper_sum (((f `\ ['a,b']) || ['a,b']),D) )
reconsider I = ['a,b'] as non empty closed_interval Subset of REAL ;
I = [.a,b.] by A1, INTEGRA5:def 3;
then ( lower_bound I = a & upper_bound I = b ) by A1, XXREAL_2:25, XXREAL_2:29;
hence ( lower_sum (((f `\ ['a,b']) || ['a,b']),D) <= (f . b) - (f . a) & (f . b) - (f . a) <= upper_sum (((f `\ ['a,b']) || ['a,b']),D) ) by A2, A3, Lm3; :: thesis: verum