theorem Th7: :: SINCOS10:7

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