theorem :: FDIFF_10:26

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 . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) )