theorem :: FDIFF_10:28

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)))) ) )