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,() such that
A2: ( f1 = g1 & g1 is_differentiable_in x0 ) by A1;
consider g2 being PartFunc of REAL,() 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 ;
A5: f1 + f2 = g1 + g2 by ;
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 ;
hence ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) by ; :: thesis: verum