theorem Th16: :: FDIFF_6:16

for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (- (exp_R * f)) & ( for x being Real st x in Z holds
f . x = - (x * (log (number_e,a))) ) & a > 0 holds
( - (exp_R * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * f)) `| Z) . x = (a #R (- x)) * (log (number_e,a)) ) )