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;
( [#] REAL = dom (AffineMap (r,0)) & ( for x being Real st x in REAL holds
(AffineMap (r,0)) . x = (r * x) + 0 ) ) by FCONT_1:def 4, FUNCT_2:def 1;
then (AffineMap (r,0)) | REAL is continuous by FDIFF_1:23, FDIFF_1:25;
then A2: (AffineMap (r,0)) | A is continuous by FCONT_1:16;
assume A3: 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 Th5;
then A4: dom (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) = dom (exp_R * (AffineMap (r,0))) by A1, FDIFF_1:def 7;
exp_R | REAL is continuous by FDIFF_1:25, SIN_COS:66;
then A5: exp_R | ((AffineMap (r,0)) .: A) is continuous by FCONT_1:16;
then (exp_R * (AffineMap (r,0))) | A is continuous by A2, FCONT_1:25;
then A6: exp_R * (AffineMap (r,0)) is_integrable_on A by A1, INTEGRA5:11;
for x being 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 A3, Th5;
then A7: ((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL = exp_R * (AffineMap (r,0)) by A4, PARTFUN1:5;
(exp_R * (AffineMap (r,0))) | A is bounded by A1, A2, A5, FCONT_1:25, 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 A3, A6, A7, Th5, INTEGRA5:13; :: thesis: verum