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

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