theorem :: FDIFF_4:41

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