theorem :: FDIFF_6:35

for Z being open Subset of REAL
for f, f1 being PartFunc of REAL,REAL st Z c= dom (ln * f) & f = exp_R - (exp_R * f1) & ( for x being Real st x in Z holds
( f1 . x = - x & f . x > 0 ) ) holds
( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * f) `| Z) . x = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) ) )