theorem :: FDIFF_9:19

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