let r be Real; :: thesis: ( r <> 0 implies ( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) ) )
assume A1: r <> 0 ; :: thesis: ( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) )
A2: [#] REAL = dom (exp_R * (AffineMap (r,0))) by FUNCT_2:def 1;
A3: [#] REAL = dom (AffineMap (r,0)) by FUNCT_2:def 1;
A4: for x being Real st x in REAL holds
(AffineMap (r,0)) . x = (r * x) + 0 by FCONT_1:def 4;
then A5: AffineMap (r,0) is_differentiable_on REAL by A3, FDIFF_1:23;
for x being Real st x in REAL holds
exp_R * (AffineMap (r,0)) is_differentiable_in x

proof

let x be Real; :: thesis: ( x in REAL implies exp_R * (AffineMap (r,0)) is_differentiable_in x )
assume x in REAL ; :: thesis: exp_R * (AffineMap (r,0)) is_differentiable_in x
then AffineMap (r,0) is_differentiable_in x by A3, A5, FDIFF_1:9;
hence exp_R * (AffineMap (r,0)) is_differentiable_in x by TAYLOR_1:19; :: thesis: verum

end;

then A6: ( [#] REAL = dom ((1 / r) (#) (exp_R * (AffineMap (r,0)))) & exp_R * (AffineMap (r,0)) is_differentiable_on REAL ) by A2, FDIFF_1:9, FUNCT_2:def 1;
hence (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL by FDIFF_1:20; :: thesis: for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x
A7: for x being Real st x in REAL holds
(((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x

proof

let x be Real; :: thesis: ( x in REAL implies (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x )
assume A8: x in REAL ; :: thesis: (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x
then A9: AffineMap (r,0) is_differentiable_in x by A3, A5, FDIFF_1:9;
(((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (1 / r) * (diff ((exp_R * (AffineMap (r,0))),x)) by A6, FDIFF_1:20, A8
.= (1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * (diff ((AffineMap (r,0)),x))) by A9, TAYLOR_1:19
.= (1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * (((AffineMap (r,0)) `| REAL) . x)) by A5, FDIFF_1:def 7, A8
.= (1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * r) by A3, A4, FDIFF_1:23, A8
.= (r * (1 / r)) * (exp_R . ((AffineMap (r,0)) . x))
.= (r / r) * (exp_R . ((AffineMap (r,0)) . x)) by XCMPLX_1:99
.= 1 * (exp_R . ((AffineMap (r,0)) . x)) by A1, XCMPLX_1:60
.= (exp_R * (AffineMap (r,0))) . x by A2, FUNCT_1:12, A8 ;
hence (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ; :: thesis: verum

end;

let x be Real; :: thesis: (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x
x in REAL by XREAL_0:def 1;
hence (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x by A7; :: thesis: verum