theorem Th43: :: INTEGR11:43

for Z being open Subset of REAL st Z c= dom ((- cot) - cosec) & ( for x being Real st x in Z holds
( 1 + (cos . x) <> 0 & 1 - (cos . x) <> 0 ) ) holds
( (- cot) - cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cot) - cosec) `| Z) . x = 1 / (1 - (cos . x)) ) )