theorem :: FDIFF_10:37

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