theorem :: FDIFF_5:24

for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) ln) & ( for x being Real st x in Z holds
x > 0 ) holds
( ((id Z) ^) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ) )