let r be Real; :: thesis: for A being non empty closed_interval Subset of REAL st r <> 0 holds
integral ((exp_R * (AffineMap (r,0))),A) = (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (upper_bound A)) - (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; :: thesis: ( r <> 0 implies integral ((exp_R * (AffineMap (r,0))),A) = (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (upper_bound A)) - (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (lower_bound A)) )
A1: dom (exp_R * (AffineMap (r,0))) = REAL by FUNCT_2:def 1;
assume A2: r <> 0 ; :: thesis: integral ((exp_R * (AffineMap (r,0))),A) = (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (upper_bound A)) - (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (lower_bound A))
then (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL by Th2;
then A3: dom (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) = dom (exp_R * (AffineMap (r,0))) by A1, FDIFF_1:def 7;
(exp_R * (AffineMap (r,0))) | A is continuous ;
then A4: exp_R * (AffineMap (r,0)) is_integrable_on A by A1, INTEGRA5:11;
for x being Element of REAL st x in dom (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) holds
(((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x by A2, Th2;
then A5: ((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL = exp_R * (AffineMap (r,0)) by A3, PARTFUN1:5;
(exp_R * (AffineMap (r,0))) | A is bounded by A1, INTEGRA5:10;
hence integral ((exp_R * (AffineMap (r,0))),A) = (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (upper_bound A)) - (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (lower_bound A)) by A2, A4, A5, Th2, INTEGRA5:13; :: thesis: verum