for r being Real
for p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 holds
grad ((r (#) f),p) = r * (grad (f,p))