theorem Th64: :: SIN_COS:65

for p being Real holds
( exp_R is_differentiable_in p & diff (exp_R,p) = exp_R . p )