theorem :: FDIFF_10:4

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