for p being Element of REAL 3
for f, g 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 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad ((f - g),p) = (grad (f,p)) - (grad (g,p))