let s, t be Real; :: thesis: 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)))
let p be Element of REAL 3; :: thesis: 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)))
let f, g be PartFunc of (REAL 3),REAL; :: thesis: ( 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 implies grad (((s (#) f) + (t (#) g)),p) = (s * (grad (f,p))) + (t * (grad (g,p))) )
assume that
A1: ( f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 ) and
A2: ( g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 ) ; :: thesis: grad (((s (#) f) + (t (#) g)),p) = (s * (grad (f,p))) + (t * (grad (g,p)))
reconsider s = s, t = t as Real ;
A3: ( s (#) f is_partial_differentiable_in p,1 & s (#) f is_partial_differentiable_in p,2 & s (#) f is_partial_differentiable_in p,3 ) by A1, PDIFF_1:33;
( t (#) g is_partial_differentiable_in p,1 & t (#) g is_partial_differentiable_in p,2 & t (#) g is_partial_differentiable_in p,3 ) by A2, PDIFF_1:33;
then grad (((s (#) f) + (t (#) g)),p) = (grad ((s (#) f),p)) + (grad ((t (#) g),p)) by A3, Th35
.= (s * (grad (f,p))) + (grad ((t (#) g),p)) by A1, Th37
.= (s * (grad (f,p))) + (t * (grad (g,p))) by A2, Th37 ;
hence grad (((s (#) f) + (t (#) g)),p) = (s * (grad (f,p))) + (t * (grad (g,p))) ; :: thesis: verum