theorem :: FDIFF_10:13

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