theorem Th11: :: INTEGRA9:11

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