theorem :: FDIFF_8:33

for Z being open Subset of REAL st Z c= dom (ln (#) cot) holds
( ln (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds
((ln (#) cot) `| Z) . x = (((cos . x) / (sin . x)) / x) - ((ln . x) / ((sin . x) ^2)) ) )