for x0 being Real
for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds
( exp_R * f is_differentiable_in x0 & diff ((exp_R * f),x0) = (exp_R . (f . x0)) * (diff (f,x0)) )