theorem :: FDIFF_4:47

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