theorem
for
s,
t being
Real 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 (
((s (#) f) + (t (#) g)),
p)
= (s * (grad (f,p))) + (t * (grad (g,p)))