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 ) ) )
A1: [#] REAL = dom (exp_R * (AffineMap (r,0))) by FUNCT_2:def 1;
A2: [#] REAL = dom (AffineMap (r,0)) by FUNCT_2:def 1;
A3: for x being Real st x in REAL holds
(AffineMap (r,0)) . x = (r * x) + 0 by FCONT_1:def 4;
then A4: AffineMap (r,0) is_differentiable_on REAL by A2, 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
AffineMap (r,0) is_differentiable_in x by A2, A4, FDIFF_1:9;
hence exp_R * (AffineMap (r,0)) is_differentiable_in x by TAYLOR_1:19; :: thesis: verum

end;

then A5: ( [#] REAL = dom ((1 / r) (#) (exp_R * (AffineMap (r,0)))) & exp_R * (AffineMap (r,0)) is_differentiable_on REAL ) by A1, FDIFF_1:9, FUNCT_2:def 1;
assume A6: 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 ) )
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 x in REAL ; :: thesis: (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x
A7: AffineMap (r,0) is_differentiable_in x by A2, A4, FDIFF_1:9;
(((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (1 / r) * (diff ((exp_R * (AffineMap (r,0))),x)) by A5, FDIFF_1:20
.= (1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * (diff ((AffineMap (r,0)),x))) by A7, TAYLOR_1:19
.= (1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * (((AffineMap (r,0)) `| REAL) . x)) by A4, FDIFF_1:def 7
.= (1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * r) by A2, A3, FDIFF_1:23
.= (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 A6, XCMPLX_1:60
.= (exp_R * (AffineMap (r,0))) . x by A1, FUNCT_1:12 ;
hence (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ; :: thesis: verum

end;

hence ( (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 ) ) by A5, FDIFF_1:20; :: thesis: verum