theorem :: FDIFF_4:43

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