let f1, f2 be PartFunc of COMPLEX ,COMPLEX ; :: thesis: for x0 being Complex 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 x0 be Complex; :: 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 and
A4: ex L being C_LINEAR ex R being C_REST st
for x being Complex st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1, Def6;
consider L1 being C_LINEAR, R1 being C_REST such that
A5: for x being Complex st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) by A4;
consider N2 being Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L being C_LINEAR ex R being C_REST st
for x being Complex st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A2, Def6;
consider L2 being C_LINEAR, R2 being C_REST such that
A8: for x being Complex st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L2 /. (x - x0)) + (R2 /. (x - x0)) by A7;
reconsider R = R1 + R2 as C_REST ;
reconsider L = L1 + L2 as C_LINEAR ;
consider N being Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Lm1;
A11: N c= dom f2 by A6, A10, XBOOLE_1:1;
N c= dom f1 by A3, A9, XBOOLE_1:1;
then N /\ N c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:27;
then A12: N c= dom (f1 + f2) by VALUED_1:def 1;

A13: now

let x be Complex; :: thesis: ( x in N implies ((f1 + f2) /. x) - ((f1 + f2) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A14: x0 in N by Th7;
assume A15: x in N ; :: thesis: ((f1 + f2) /. x) - ((f1 + f2) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence ((f1 + f2) /. x) - ((f1 + f2) /. x0) = ((f1 /. x) + (f2 /. x)) - ((f1 + f2) /. x0) by A12, CFUNCT_1:3
.= ((f1 /. x) + (f2 /. x)) - ((f1 /. x0) + (f2 /. x0)) by A12, A14, CFUNCT_1:3
.= ((f1 /. x) - (f1 /. x0)) + ((f2 /. x) - (f2 /. x0))
.= ((L1 /. (x - x0)) + (R1 /. (x - x0))) + ((f2 /. x) - (f2 /. x0)) by A5, A9, A15
.= ((L1 /. (x - x0)) + (R1 /. (x - x0))) + ((L2 /. (x - x0)) + (R2 /. (x - x0))) by A8, A10, A15
.= ((L1 /. (x - x0)) + (L2 /. (x - x0))) + ((R1 /. (x - x0)) + (R2 /. (x - x0)))
.= (L /. (x - x0)) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) by CFUNCT_1:76
.= (L /. (x - x0)) + (R /. (x - x0)) by CFUNCT_1:76 ;
:: thesis: verum

end;

hence f1 + f2 is_differentiable_in x0 by A12, Def6; :: thesis: diff (f1 + f2),x0 = (diff f1,x0) + (diff f2,x0)
hence diff (f1 + f2),x0 = L /. 1r by A12, A13, Def7
.= (L1 /. 1r ) + (L2 /. 1r ) by CFUNCT_1:76
.= (diff f1,x0) + (L2 /. 1r ) by A1, A3, A5, Def7
.= (diff f1,x0) + (diff f2,x0) by A2, A6, A8, Def7 ;
:: thesis: verum