let A be non empty closed_interval Subset of REAL; :: thesis: integral (((AffineMap (1,0)) (#) exp_R),A) = ((exp_R (#) (AffineMap (1,(- 1)))) . (upper_bound A)) - ((exp_R (#) (AffineMap (1,(- 1)))) . (lower_bound A))
A1: for x being Real st x in REAL holds
(AffineMap (1,(- 1))) . x = x - 1

proof

let x be Real; :: thesis: ( x in REAL implies (AffineMap (1,(- 1))) . x = x - 1 )
assume x in REAL ; :: thesis: (AffineMap (1,(- 1))) . x = x - 1
(AffineMap (1,(- 1))) . x = (1 * x) + (- 1) by FCONT_1:def 4
.= x - 1 ;
hence (AffineMap (1,(- 1))) . x = x - 1 ; :: thesis: verum

end;

A2: dom (exp_R (#) (AffineMap (1,(- 1)))) = [#] REAL by FUNCT_2:def 1;
A3: for x being Real st x in REAL holds
((AffineMap (1,0)) (#) exp_R) . x = x * (exp_R . x)

proof

let x be Real; :: thesis: ( x in REAL implies ((AffineMap (1,0)) (#) exp_R) . x = x * (exp_R . x) )
assume x in REAL ; :: thesis: ((AffineMap (1,0)) (#) exp_R) . x = x * (exp_R . x)
((AffineMap (1,0)) (#) exp_R) . x = ((AffineMap (1,0)) . x) * (exp_R . x) by VALUED_1:5
.= ((1 * x) + 0) * (exp_R . x) by FCONT_1:def 4
.= x * (exp_R . x) ;
hence ((AffineMap (1,0)) (#) exp_R) . x = x * (exp_R . x) ; :: thesis: verum

end;

A4: for x being Element of REAL st x in dom ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) holds
((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . x = ((AffineMap (1,0)) (#) exp_R) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) implies ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . x = ((AffineMap (1,0)) (#) exp_R) . x )
assume x in dom ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) ; :: thesis: ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . x = ((AffineMap (1,0)) (#) exp_R) . x
((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . x = x * (exp_R . x) by A2, A1, FDIFF_4:55
.= ((AffineMap (1,0)) (#) exp_R) . x by A3 ;
hence ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . x = ((AffineMap (1,0)) (#) exp_R) . x ; :: thesis: verum

end;

A5: [#] REAL = dom ((AffineMap (1,0)) (#) exp_R) by FUNCT_2:def 1;
((AffineMap (1,0)) (#) exp_R) | A is continuous ;
then A6: (AffineMap (1,0)) (#) exp_R is_integrable_on A by A5, INTEGRA5:11;
exp_R (#) (AffineMap (1,(- 1))) is_differentiable_on REAL by A2, A1, FDIFF_4:55;
then dom ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) = dom ((AffineMap (1,0)) (#) exp_R) by A5, FDIFF_1:def 7;
then A7: (exp_R (#) (AffineMap (1,(- 1)))) `| REAL = (AffineMap (1,0)) (#) exp_R by A4, PARTFUN1:5;
((AffineMap (1,0)) (#) exp_R) | A is bounded by A5, INTEGRA5:10;
hence integral (((AffineMap (1,0)) (#) exp_R),A) = ((exp_R (#) (AffineMap (1,(- 1)))) . (upper_bound A)) - ((exp_R (#) (AffineMap (1,(- 1)))) . (lower_bound A)) by A2, A1, A6, A7, FDIFF_4:55, INTEGRA5:13; :: thesis: verum