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 & f is_differentiable_on X ) and
A2: f `| X is_integrable_on A and
A3: (f `| X) | A is bounded ; :: thesis: integral (f `| X),A = (f . (sup A)) - (f . (inf A))
(f `| X) || A is integrable by A2, Def2;
then A4: upper_integral ((f `| X) || A) = lower_integral ((f `| X) || A) by INTEGRA1:def 17;
A5: 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
A6: ( 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 A6, INTEGRA1:def 11;
hence (f . (sup A)) - (f . (inf A)) <= r by A1, A3, Th12; :: thesis: verum

end;

dom (upper_sum_set ((f `| X) || A)) = divs A by INTEGRA1:def 11;
then not rng (upper_sum_set ((f `| X) || A)) is empty by RELAT_1:65;
then (f . (sup A)) - (f . (inf A)) <= inf (rng (upper_sum_set ((f `| X) || A))) by A5, SEQ_4:60;
then A7: upper_integral ((f `| X) || A) >= (f . (sup A)) - (f . (inf A)) by INTEGRA1:def 15;
A8: 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
A9: ( 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 A9, INTEGRA1:def 12;
hence r <= (f . (sup A)) - (f . (inf A)) by A1, A3, Th12; :: thesis: verum

end;

dom (lower_sum_set ((f `| X) || A)) = divs A by INTEGRA1:def 12;
then not rng (lower_sum_set ((f `| X) || A)) is empty by RELAT_1:65;
then sup (rng (lower_sum_set ((f `| X) || A))) <= (f . (sup A)) - (f . (inf A)) by A8, SEQ_4:62;
then upper_integral ((f `| X) || A) <= (f . (sup A)) - (f . (inf A)) by A4, INTEGRA1:def 16;
then upper_integral ((f `| X) || A) = (f . (sup A)) - (f . (inf A)) by A7, XXREAL_0:1;
hence integral (f `| X),A = (f . (sup A)) - (f . (inf A)) by INTEGRA1:def 18; :: thesis: verum