let x0 be Real; :: thesis: for n being non zero Element of NAT
for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
let n be non zero Element of NAT ; :: thesis: for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
let f1, f2 be PartFunc of REAL,(REAL n); :: thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) )
assume A1: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) ; :: thesis: ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
consider g1 being PartFunc of REAL,(REAL-NS n) such that
A2: ( f1 = g1 & g1 is_differentiable_in x0 ) by A1;
consider g2 being PartFunc of REAL,(REAL-NS n) such that
A3: ( f2 = g2 & g2 is_differentiable_in x0 ) by A1;
A4: ( g1 + g2 is_differentiable_in x0 & diff ((g1 + g2),x0) = (diff (g1,x0)) + (diff (g2,x0)) ) by A2, A3, NDIFF_3:14;
A5: f1 + f2 = g1 + g2 by A2, A3, NFCONT_4:5;
A6: ( diff (f1,x0) = diff (g1,x0) & diff (f2,x0) = diff (g2,x0) ) by A2, A3, Th3;
diff ((f1 + f2),x0) = diff ((g1 + g2),x0) by A2, A3, Th3, NFCONT_4:5;
hence ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) by A5, A4, A6, REAL_NS1:2; :: thesis: verum