let A be closed-interval Subset of REAL ; :: thesis: for X being set
for f being PartFunc of REAL ,REAL st A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded holds
integral (f `| X),A = (f . (sup A)) - (f . (inf A))
let X be set ; :: thesis: for f being PartFunc of REAL ,REAL st A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded holds
integral (f `| X),A = (f . (sup A)) - (f . (inf A))
let f be PartFunc of REAL ,REAL ; :: thesis: ( A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded implies integral (f `| X),A = (f . (sup A)) - (f . (inf A)) )
assume that
A1: A c= X and
A2: f is_differentiable_on X and
A3: f `| X is_integrable_on A and
A4: (f `| X) | A is bounded ; :: thesis: integral (f `| X),A = (f . (sup A)) - (f . (inf A))
(f `| X) || A is integrable by A3, Def2;
then A5: ( (f `| X) || A is upper_integrable & (f `| X) || A is lower_integrable & upper_integral ((f `| X) || A) = lower_integral ((f `| X) || A) ) by INTEGRA1:def 17;
dom (upper_sum_set ((f `| X) || A)) = divs A by INTEGRA1:def 11;
then A6: not rng (upper_sum_set ((f `| X) || A)) is empty by RELAT_1:65;
dom (lower_sum_set ((f `| X) || A)) = divs A by INTEGRA1:def 12;
then A7: not rng (lower_sum_set ((f `| X) || A)) is empty by RELAT_1:65;
for r being real number st r in rng (lower_sum_set ((f `| X) || A)) holds
r <= (f . (sup A)) - (f . (inf A))

proof

let r be real number ; :: thesis: ( r in rng (lower_sum_set ((f `| X) || A)) implies r <= (f . (sup A)) - (f . (inf A)) )
assume r in rng (lower_sum_set ((f `| X) || A)) ; :: thesis: r <= (f . (sup A)) - (f . (inf A))
then consider D being Element of divs A such that
A8: ( D in dom (lower_sum_set ((f `| X) || A)) & r = (lower_sum_set ((f `| X) || A)) . D ) by PARTFUN1:26;
reconsider D = D as Division of A by INTEGRA1:def 3;
r = lower_sum ((f `| X) || A),D by A8, INTEGRA1:def 12;
hence r <= (f . (sup A)) - (f . (inf A)) by A1, A2, A4, Th12; :: thesis: verum

end;

then sup (rng (lower_sum_set ((f `| X) || A))) <= (f . (sup A)) - (f . (inf A)) by A7, SEQ_4:62;
then A9: upper_integral ((f `| X) || A) <= (f . (sup A)) - (f . (inf A)) by A5, INTEGRA1:def 16;
for r being real number st r in rng (upper_sum_set ((f `| X) || A)) holds
(f . (sup A)) - (f . (inf A)) <= r

proof

let r be real number ; :: thesis: ( r in rng (upper_sum_set ((f `| X) || A)) implies (f . (sup A)) - (f . (inf A)) <= r )
assume r in rng (upper_sum_set ((f `| X) || A)) ; :: thesis: (f . (sup A)) - (f . (inf A)) <= r
then consider D being Element of divs A such that
A10: ( D in dom (upper_sum_set ((f `| X) || A)) & r = (upper_sum_set ((f `| X) || A)) . D ) by PARTFUN1:26;
reconsider D = D as Division of A by INTEGRA1:def 3;
r = upper_sum ((f `| X) || A),D by A10, INTEGRA1:def 11;
hence (f . (sup A)) - (f . (inf A)) <= r by A1, A2, A4, Th12; :: thesis: verum

end;

then (f . (sup A)) - (f . (inf A)) <= inf (rng (upper_sum_set ((f `| X) || A))) by A6, SEQ_4:60;
then upper_integral ((f `| X) || A) >= (f . (sup A)) - (f . (inf A)) by INTEGRA1:def 15;
then upper_integral ((f `| X) || A) = (f . (sup A)) - (f . (inf A)) by A9, XXREAL_0:1;
hence integral (f `| X),A = (f . (sup A)) - (f . (inf A)) by INTEGRA1:def 18; :: thesis: verum