theorem Th8: :: INTEGR14:8

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