let n, m be non zero Nat; :: thesis: for g1, g2 being PartFunc of (REAL m),(REAL n)
for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds
( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) )
let g1, g2 be PartFunc of (REAL m),(REAL n); :: thesis: for y0 being Element of REAL m st g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds
( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) )
let y0 be Element of REAL m; :: thesis: ( g1 is_differentiable_in y0 & g2 is_differentiable_in y0 implies ( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) ) )
assume A1: ( g1 is_differentiable_in y0 & g2 is_differentiable_in y0 ) ; :: thesis: ( g1 + g2 is_differentiable_in y0 & diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) )
reconsider f1 = g1 as PartFunc of (REAL-NS m),(REAL-NS n) by Th1;
reconsider f2 = g2 as PartFunc of (REAL-NS m),(REAL-NS n) by Th1;
reconsider x0 = y0 as Point of (REAL-NS m) by REAL_NS1:def 4;
( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A1, Th2;
then A2: ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) by NDIFF_1:35;
f1 + f2 = g1 + g2 by Th4;
hence g1 + g2 is_differentiable_in y0 by A2, Th2; :: thesis: diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0))
then A3: diff ((g1 + g2),y0) = diff ((f1 + f2),x0) by Th4, Th3;
( diff (f1,x0) = diff (g1,y0) & diff (f2,x0) = diff (g2,y0) ) by Th3, A1;
hence diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) by A2, A3, Th7; :: thesis: verum