theorem Th62: :: SIN_COS:63

for p being Real holds
( cos is_differentiable_in p & diff (cos,p) = - (sin . p) )