let A be 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: dom (exp_R (#) (AffineMap 1,(- 1))) = [#] REAL by FUNCT_2:def 1;
A2: dom (AffineMap 1,0 ) = [#] REAL by FUNCT_2:def 1;
B1: [#] REAL = dom ((AffineMap 1,0 ) (#) exp_R ) by FUNCT_2:def 1;
A3: 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 JORDAN16:def 3
.= x - 1 ;
hence (AffineMap 1,(- 1)) . x = x - 1 ; :: thesis: verum

end;

A4: for x being Real st x in REAL holds
(AffineMap 1,0 ) . x = (1 * x) + 0 by JORDAN16:def 3;
C1: AffineMap 1,0 is_differentiable_on REAL by A2, A4, FDIFF_1:31;
(AffineMap 1,0 ) (#) exp_R is_differentiable_on REAL by B1, C1, FDIFF_1:29, TAYLOR_1:16;
then ((AffineMap 1,0 ) (#) exp_R ) | REAL is continuous by FDIFF_1:33;
then ((AffineMap 1,0 ) (#) exp_R ) | A is continuous by FCONT_1:17;
then A5: ( (AffineMap 1,0 ) (#) exp_R is_integrable_on A & ((AffineMap 1,0 ) (#) exp_R ) | A is bounded ) by B1, INTEGRA5:10, INTEGRA5:11;
A6: exp_R (#) (AffineMap 1,(- 1)) is_differentiable_on REAL by A1, A3, FDIFF_4:55;
B: 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 JORDAN16:def 3
.= x * (exp_R . x) ;
hence ((AffineMap 1,0 ) (#) exp_R ) . x = x * (exp_R . x) ; :: thesis: verum

end;

A7: for x being 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 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 A1, A3, FDIFF_4:55
.= ((AffineMap 1,0 ) (#) exp_R ) . x by B ;
hence ((exp_R (#) (AffineMap 1,(- 1))) `| REAL ) . x = ((AffineMap 1,0 ) (#) exp_R ) . x ; :: thesis: verum

end;

dom ((exp_R (#) (AffineMap 1,(- 1))) `| REAL ) = dom ((AffineMap 1,0 ) (#) exp_R ) by B1, A6, FDIFF_1:def 8;
then (exp_R (#) (AffineMap 1,(- 1))) `| REAL = (AffineMap 1,0 ) (#) exp_R by A7, PARTFUN1:34;
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 A1, A3, A5, FDIFF_4:55, INTEGRA5:13; :: thesis: verum