theorem Th2: :: FDIFF_9:2

for x being Real st sin . x <> 0 holds
( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )