theorem :: FDIFF_6:22

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