A1: [#] REAL = dom (exp_R * (AffineMap ((- 1),0))) by FUNCT_2:def 1;
A2: [#] REAL = dom (AffineMap ((- jj),0)) by FUNCT_2:def 1;
A3: for x being Real st x in REAL holds
(AffineMap ((- 1),0)) . x = ((- 1) * x) + 0 by FCONT_1:def 4;
then A4: AffineMap ((- jj),0) is_differentiable_on REAL by A2, FDIFF_1:23;
for x being Real st x in REAL holds
exp_R * (AffineMap ((- 1),0)) is_differentiable_in x

proof

let x be Real; :: thesis: ( x in REAL implies exp_R * (AffineMap ((- 1),0)) is_differentiable_in x )
assume x in REAL ; :: thesis: exp_R * (AffineMap ((- 1),0)) is_differentiable_in x
then AffineMap ((- jj),0) is_differentiable_in x by A2, A4, FDIFF_1:9;
hence exp_R * (AffineMap ((- 1),0)) is_differentiable_in x by TAYLOR_1:19; :: thesis: verum

end;

then A5: exp_R * (AffineMap ((- 1),0)) is_differentiable_on REAL by A1, FDIFF_1:9;
hence - (exp_R * (AffineMap ((- 1),0))) is_differentiable_on REAL by Lm1, FDIFF_1:20; :: thesis: for x being Real holds ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x)
A6: for x being Real st x in REAL holds
((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x)

proof

let x be Real; :: thesis: ( x in REAL implies ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) )
assume A7: x in REAL ; :: thesis: ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x)
then A8: AffineMap ((- 1),0) is_differentiable_in x by A2, A4, FDIFF_1:9;
((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = (- 1) * (diff ((exp_R * (AffineMap ((- 1),0))),x)) by A5, Lm1, FDIFF_1:20, A7
.= (- 1) * ((exp_R . ((AffineMap ((- 1),0)) . x)) * (diff ((AffineMap ((- 1),0)),x))) by A8, TAYLOR_1:19
.= (- 1) * ((exp_R . ((AffineMap ((- 1),0)) . x)) * (((AffineMap ((- 1),0)) `| REAL) . x)) by A4, FDIFF_1:def 7, A7
.= (- 1) * ((exp_R . ((AffineMap ((- 1),0)) . x)) * (- 1)) by A2, A3, FDIFF_1:23, A7
.= (- 1) * ((exp_R . (((- 1) * x) + 0)) * (- 1)) by FCONT_1:def 4
.= exp_R (- x) ;
hence ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) ; :: thesis: verum

end;

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