theorem Th49: :: INTEGR11:49

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) / (1 + (cos . x)) ) )