theorem Th8: :: SINCOS10:8

( cosec is_differentiable_on ].0,(PI / 2).[ & ( for x being Real st x in ].0,(PI / 2).[ holds
diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) )