theorem Th10: :: INTEGRA9:10

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