let a, b be Real; :: thesis: for f being PartFunc of REAL,REAL st a < b & f is_differentiable_on_interval ['a,b'] & f `\ ['a,b'] is_integrable_on ['a,b'] & f `\ ['a,b'] is bounded holds
integral ((f `\ ['a,b']),['a,b']) = (f . b) - (f . a)
let f be PartFunc of REAL,REAL; :: thesis: ( a < b & f is_differentiable_on_interval ['a,b'] & f `\ ['a,b'] is_integrable_on ['a,b'] & f `\ ['a,b'] is bounded implies integral ((f `\ ['a,b']),['a,b']) = (f . b) - (f . a) )
assume that
A1: a < b and
A2: f is_differentiable_on_interval ['a,b'] and
A3: f `\ ['a,b'] is_integrable_on ['a,b'] and
A4: f `\ ['a,b'] is bounded ; :: thesis: integral ((f `\ ['a,b']),['a,b']) = (f . b) - (f . a)
reconsider I = ['a,b'] as non empty closed_interval Subset of REAL ;
A5: (f `\ I) || I is integrable by A3;
for r being Real st r in rng (upper_sum_set ((f `\ I) || I)) holds
(f . b) - (f . a) <= r

proof

let r be Real; :: thesis: ( r in rng (upper_sum_set ((f `\ I) || I)) implies (f . b) - (f . a) <= r )
assume r in rng (upper_sum_set ((f `\ I) || I)) ; :: thesis: (f . b) - (f . a) <= r
then consider D being Element of divs I such that
A6: ( D in dom (upper_sum_set ((f `\ I) || I)) & r = (upper_sum_set ((f `\ I) || I)) . D ) by PARTFUN1:3;
reconsider D = D as Division of I by INTEGRA1:def 3;
r = upper_sum (((f `\ I) || I),D) by A6, INTEGRA1:def 10;
hence (f . b) - (f . a) <= r by A2, A4, A1, Th43; :: thesis: verum

end;

then A7: (f . b) - (f . a) <= lower_bound (rng (upper_sum_set ((f `\ I) || I))) by SEQ_4:43;
for r being Real st r in rng (lower_sum_set ((f `\ I) || I)) holds
r <= (f . b) - (f . a)

proof

let r be Real; :: thesis: ( r in rng (lower_sum_set ((f `\ I) || I)) implies r <= (f . b) - (f . a) )
assume r in rng (lower_sum_set ((f `\ I) || I)) ; :: thesis: r <= (f . b) - (f . a)
then consider D being Element of divs I such that
A8: ( D in dom (lower_sum_set ((f `\ I) || I)) & r = (lower_sum_set ((f `\ I) || I)) . D ) by PARTFUN1:3;
reconsider D = D as Division of I by INTEGRA1:def 3;
r = lower_sum (((f `\ I) || I),D) by A8, INTEGRA1:def 11;
hence r <= (f . b) - (f . a) by A2, A4, A1, Th43; :: thesis: verum

end;

then upper_bound (rng (lower_sum_set ((f `\ I) || I))) <= (f . b) - (f . a) by SEQ_4:45;
hence integral ((f `\ ['a,b']),['a,b']) = (f . b) - (f . a) by A5, A7, XXREAL_0:1; :: thesis: verum