theorem Th12: :: INTEGR14:12

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