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 B: 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 ) )
A: [#] REAL = dom ((1 / r) (#) (exp_R * (AffineMap r,0 ))) by FUNCT_2:def 1;
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 JORDAN16:def 3;
then A4: ( AffineMap r,0 is_differentiable_on REAL & ( for x being Real st x in [#] REAL holds
((AffineMap r,0 ) `| REAL ) . x = r ) ) by A2, FDIFF_1:31;
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 A4, FDIFF_1:16;
hence exp_R * (AffineMap r,0 ) is_differentiable_in x by TAYLOR_1:19; :: thesis: verum

end;

then A5: exp_R * (AffineMap r,0 ) is_differentiable_on REAL by A1, FDIFF_1:16;
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
A6: AffineMap r,0 is_differentiable_in x by A4, FDIFF_1:16;
(((1 / r) (#) (exp_R * (AffineMap r,0 ))) `| REAL ) . x = (1 / r) * (diff (exp_R * (AffineMap r,0 )),x) by A, A5, FDIFF_1:28
.= (1 / r) * ((exp_R . ((AffineMap r,0 ) . x)) * (diff (AffineMap r,0 ),x)) by A6, TAYLOR_1:19
.= (1 / r) * ((exp_R . ((AffineMap r,0 ) . x)) * (((AffineMap r,0 ) `| REAL ) . x)) by A4, FDIFF_1:def 8
.= (1 / r) * ((exp_R . ((AffineMap r,0 ) . x)) * r) by A2, A3, FDIFF_1:31
.= (r * (1 / r)) * (exp_R . ((AffineMap r,0 ) . x))
.= (r / r) * (exp_R . ((AffineMap r,0 ) . x)) by XCMPLX_1:100
.= 1 * (exp_R . ((AffineMap r,0 ) . x)) by B, XCMPLX_1:60
.= (exp_R * (AffineMap r,0 )) . x by A1, FUNCT_1:22 ;
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, A, FDIFF_1:28; :: thesis: verum