theorem Th51: :: INTEGR11:51

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