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 (f - g),p = (grad f,p) - (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 (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 ) ; :: thesis: 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 Th43
.= |[((partdiff f,p,1) - (partdiff g,p,1)),(partdiff (f - g),p,2),(partdiff (f - g),p,3)]| by A1, A2, PDIFF_1:31
.= |[((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:31
.= |[((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:31
.= |[((partdiff f,p,1) + (- (partdiff g,p,1))),((partdiff f,p,2) + (- (partdiff g,p,2))),((partdiff f,p,3) + (- (partdiff g,p,3)))]|
.= |[(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 Lm6
.= (grad f,p) + |[((- 1) * (partdiff g,p,1)),((- 1) * (partdiff g,p,2)),((- 1) * (partdiff g,p,3))]| by Th43
.= (grad f,p) + ((- 1) * |[(partdiff g,p,1),(partdiff g,p,2),(partdiff g,p,3)]|) by EUCLID_8:59
.= (grad f,p) - (grad g,p) by Th43 ;
hence grad (f - g),p = (grad f,p) - (grad g,p) ; :: thesis: verum