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