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