let r be Real; 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; ( 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
; 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; verum