theorem :: FDIFF_10:19

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