let n, m be non empty Element of 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 AS: ( 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 DPREP010;
reconsider f2 = g2 as PartFunc of (REAL-NS m),(REAL-NS n) by DPREP010;
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 AS, DPREP020;
then P2: ( f1 + f2 is_differentiable_in x0 & diff (f1 + f2),x0 = (diff f1,x0) + (diff f2,x0) ) by NDIFF_1:40;
f1 + f2 = g1 + g2 by DPREP040;
hence g1 + g2 is_differentiable_in y0 by P2, DPREP020; :: thesis: diff (g1 + g2),y0 = (diff g1,y0) + (diff g2,y0)
then P4: diff (g1 + g2),y0 = diff (f1 + f2),x0 by DPREP040, DPREP030;
( diff f1,x0 = diff g1,y0 & diff f2,x0 = diff g2,y0 ) by DPREP030, AS;
hence diff (g1 + g2),y0 = (diff g1,y0) + (diff g2,y0) by P2, P4, DPREP070; :: thesis: verum