theorem Th65: :: SIN_COS:66

for th being Real holds
( exp_R is_differentiable_on REAL & diff (exp_R,th) = exp_R . th )