let s, t be 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)))
let p be 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 f, g be PartFunc of (REAL 3),REAL; ( 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 )
; 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)))
; verum