theorem :: FDIFF_5:25

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