theorem :: INTEGRA9:1

( - (exp_R * (AffineMap ((- 1),0))) is_differentiable_on REAL & ( for x being Real holds ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) ) )