let m be non zero Element of NAT ; :: thesis: for f, g being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_differentiable_in x & g is_differentiable_in x holds
( f + g is_differentiable_in x & diff ((f + g),x) = (diff (f,x)) + (diff (g,x)) & f - g is_differentiable_in x & diff ((f - g),x) = (diff (f,x)) - (diff (g,x)) )
let f, g be PartFunc of (REAL m),REAL; :: thesis: for x being Element of REAL m st f is_differentiable_in x & g is_differentiable_in x holds
( f + g is_differentiable_in x & diff ((f + g),x) = (diff (f,x)) + (diff (g,x)) & f - g is_differentiable_in x & diff ((f - g),x) = (diff (f,x)) - (diff (g,x)) )
let x be Element of REAL m; :: thesis: ( f is_differentiable_in x & g is_differentiable_in x implies ( f + g is_differentiable_in x & diff ((f + g),x) = (diff (f,x)) + (diff (g,x)) & f - g is_differentiable_in x & diff ((f - g),x) = (diff (f,x)) - (diff (g,x)) ) )
assume ( f is_differentiable_in x & g is_differentiable_in x ) ; :: thesis: ( f + g is_differentiable_in x & diff ((f + g),x) = (diff (f,x)) + (diff (g,x)) & f - g is_differentiable_in x & diff ((f - g),x) = (diff (f,x)) - (diff (g,x)) )
then A1: ( <>* f is_differentiable_in x & <>* g is_differentiable_in x ) ;
then A2: ( (<>* f) + (<>* g) is_differentiable_in x & (<>* f) - (<>* g) is_differentiable_in x ) by PDIFF_6:20, PDIFF_6:21;
hence f + g is_differentiable_in x by Th7; :: thesis: ( diff ((f + g),x) = (diff (f,x)) + (diff (g,x)) & f - g is_differentiable_in x & diff ((f - g),x) = (diff (f,x)) - (diff (g,x)) )
thus diff ((f + g),x) = (proj (1,1)) * (diff (((<>* f) + (<>* g)),x)) by Th7
.= (proj (1,1)) * ((diff ((<>* f),x)) + (diff ((<>* g),x))) by A1, PDIFF_6:20
.= (diff (f,x)) + (diff (g,x)) by INTEGR15:15 ; :: thesis: ( f - g is_differentiable_in x & diff ((f - g),x) = (diff (f,x)) - (diff (g,x)) )
thus f - g is_differentiable_in x by A2, Th7; :: thesis: diff ((f - g),x) = (diff (f,x)) - (diff (g,x))
thus diff ((f - g),x) = (proj (1,1)) * (diff (((<>* f) - (<>* g)),x)) by Th7
.= (proj (1,1)) * ((diff ((<>* f),x)) - (diff ((<>* g),x))) by A1, PDIFF_6:21
.= (diff (f,x)) - (diff (g,x)) by INTEGR15:15 ; :: thesis: verum