theorem Th14: :: INTEGR14:14

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