let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL ,REAL 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 ; :: 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 that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0 ; :: thesis: ( f1 + f2 is_differentiable_in x0 & diff (f1 + f2),x0 = (diff f1,x0) + (diff f2,x0) )
consider N1 being Neighbourhood of x0 such that
A3: ( N1 c= dom f1 & ex L being LINEAR ex R being REST st
for x being Real st x in N1 holds
(f1 . x) - (f1 . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A1, Def5;
consider L1 being LINEAR, R1 being REST such that
A4: for x being Real st x in N1 holds
(f1 . x) - (f1 . x0) = (L1 . (x - x0)) + (R1 . (x - x0)) by A3;
consider N2 being Neighbourhood of x0 such that
A5: ( N2 c= dom f2 & ex L being LINEAR ex R being REST st
for x being Real st x in N2 holds
(f2 . x) - (f2 . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A2, Def5;
consider L2 being LINEAR, R2 being REST such that
A6: for x being Real st x in N2 holds
(f2 . x) - (f2 . x0) = (L2 . (x - x0)) + (R2 . (x - x0)) by A5;
consider N being Neighbourhood of x0 such that
A7: ( N c= N1 & N c= N2 ) by RCOMP_1:38;
reconsider L = L1 + L2 as LINEAR by Th6;
A8: ( L1 is total & L2 is total ) by Def4;
reconsider R = R1 + R2 as REST by Th8;
A9: ( R1 is total & R2 is total ) by Def3;
A10: N c= dom f1 by A3, A7, XBOOLE_1:1;
N c= dom f2 by A5, A7, XBOOLE_1:1;
then N /\ N c= (dom f1) /\ (dom f2) by A10, XBOOLE_1:27;
then A11: N c= dom (f1 + f2) by VALUED_1:def 1;

A12: now

let x be Real; :: thesis: ( x in N implies ((f1 + f2) . x) - ((f1 + f2) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A13: x in N ; :: thesis: ((f1 + f2) . x) - ((f1 + f2) . x0) = (L . (x - x0)) + (R . (x - x0))
A14: x0 in N by RCOMP_1:37;
thus ((f1 + f2) . x) - ((f1 + f2) . x0) = ((f1 . x) + (f2 . x)) - ((f1 + f2) . x0) by A11, A13, VALUED_1:def 1
.= ((f1 . x) + (f2 . x)) - ((f1 . x0) + (f2 . x0)) by A11, A14, VALUED_1:def 1
.= ((f1 . x) - (f1 . x0)) + ((f2 . x) - (f2 . x0))
.= ((L1 . (x - x0)) + (R1 . (x - x0))) + ((f2 . x) - (f2 . x0)) by A4, A7, A13
.= ((L1 . (x - x0)) + (R1 . (x - x0))) + ((L2 . (x - x0)) + (R2 . (x - x0))) by A6, A7, A13
.= ((L1 . (x - x0)) + (L2 . (x - x0))) + ((R1 . (x - x0)) + (R2 . (x - x0)))
.= (L . (x - x0)) + ((R1 . (x - x0)) + (R2 . (x - x0))) by A8, RFUNCT_1:72
.= (L . (x - x0)) + (R . (x - x0)) by A9, RFUNCT_1:72 ; :: thesis: verum

end;

hence f1 + f2 is_differentiable_in x0 by A11, Def5; :: thesis: diff (f1 + f2),x0 = (diff f1,x0) + (diff f2,x0)
hence diff (f1 + f2),x0 = L . 1 by A11, A12, Def6
.= (L1 . 1) + (L2 . 1) by A8, RFUNCT_1:72
.= (diff f1,x0) + (L2 . 1) by A1, A3, A4, Def6
.= (diff f1,x0) + (diff f2,x0) by A2, A5, A6, Def6 ;
:: thesis: verum