theorem :: FDIFF_10:38

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