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 ((f + g),p) = (grad (f,p)) + (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 ((f + g),p) = (grad (f,p)) + (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 ((f + g),p) = (grad (f,p)) + (grad (g,p))
grad ((f + g),p) =
|[(partdiff ((f + g),p,1)),(partdiff ((f + g),p,2)),(partdiff ((f + g),p,3))]|
by Th34
.=
|[((partdiff (f,p,1)) + (partdiff (g,p,1))),(partdiff ((f + g),p,2)),(partdiff ((f + g),p,3))]|
by A1, A2, PDIFF_1:29
.=
|[((partdiff (f,p,1)) + (partdiff (g,p,1))),((partdiff (f,p,2)) + (partdiff (g,p,2))),(partdiff ((f + g),p,3))]|
by A1, A2, PDIFF_1:29
.=
|[((partdiff (f,p,1)) + (partdiff (g,p,1))),((partdiff (f,p,2)) + (partdiff (g,p,2))),((partdiff (f,p,3)) + (partdiff (g,p,3)))]|
by A1, A2, PDIFF_1:29
.=
|[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]| + |[(partdiff (g,p,1)),(partdiff (g,p,2)),(partdiff (g,p,3))]|
by Lm4
.=
(grad (f,p)) + |[(partdiff (g,p,1)),(partdiff (g,p,2)),(partdiff (g,p,3))]|
by Th34
.=
(grad (f,p)) + (grad (g,p))
by Th34
;
hence
grad ((f + g),p) = (grad (f,p)) + (grad (g,p))
; verum