let F be non trivial RealNormSpace; :: thesis: for x0 being Real
for f1, f2 being PartFunc of REAL, the carrier of F 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 Real; :: thesis: for f1, f2 being PartFunc of REAL, the carrier of F 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, the carrier of F; :: 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 LINEAR of F ex R being REST of F st
for x being Real st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def3;
consider L1 being LINEAR of F, R1 being REST of F such that
A5: for x being Real 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 LINEAR of F ex R being REST of F st
for x being Real st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2, Def3;
consider L2 being LINEAR of F, R2 being REST of F such that
A8: for x being Real st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L2 . (x - x0)) + (R2 /. (x - x0)) by A7;
reconsider R = R1 + R2 as REST of F by Th7;
reconsider L = L1 + L2 as LINEAR of F by Th3;
A9: ( dom L1 = REAL & dom L2 = REAL ) by FUNCT_2:def 1;
consider N being Neighbourhood of x0 such that
A10: N c= N1 and
A11: N c= N2 by RCOMP_1:17;
A12: N c= dom f2 by A6, A11, XBOOLE_1:1;
N c= dom f1 by A3, A10, XBOOLE_1:1;
then N /\ N c= (dom f1) /\ (dom f2) by A12, XBOOLE_1:27;
then A13: N c= dom (f1 + f2) by VFUNCT_1:def 1;
( R1 is total & R2 is total ) by Def1;
then R1 + R2 is total by VFUNCT_1:32;
then A14: dom (R1 + R2) = REAL by FUNCT_2:def 1;
L1 + L2 is total by VFUNCT_1:32;
then A15: dom (L1 + L2) = REAL by FUNCT_2:def 1;

A16: now

let x be Real; :: thesis: ( x in N implies ((f1 + f2) /. x) - ((f1 + f2) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A17: x0 in N by RCOMP_1:16;
assume A18: 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 A13, VFUNCT_1:def 1
.= ((f1 /. x) + (f2 /. x)) - ((f1 /. x0) + (f2 /. x0)) by A13, A17, VFUNCT_1:def 1
.= (f1 /. x) + ((f2 /. x) - ((f1 /. x0) + (f2 /. x0))) by RLVECT_1:28
.= (f1 /. x) + (((f2 /. x) - (f2 /. x0)) - (f1 /. x0)) by RLVECT_1:27
.= ((f1 /. x) + ((f2 /. x) - (f2 /. x0))) - (f1 /. x0) by RLVECT_1:28
.= ((f2 /. x) - (f2 /. x0)) + ((f1 /. x) - (f1 /. x0)) by RLVECT_1:28
.= ((L1 . (x - x0)) + (R1 /. (x - x0))) + ((f2 /. x) - (f2 /. x0)) by A5, A10, A18
.= ((L1 . (x - x0)) + (R1 /. (x - x0))) + ((L2 . (x - x0)) + (R2 /. (x - x0))) by A8, A11, A18
.= (((L1 . (x - x0)) + (R1 /. (x - x0))) + (L2 . (x - x0))) + (R2 /. (x - x0)) by RLVECT_1:def 3
.= (((L1 . (x - x0)) + (L2 . (x - x0))) + (R1 /. (x - x0))) + (R2 /. (x - x0)) by RLVECT_1:def 3
.= ((L1 /. (x - x0)) + (L2 /. (x - x0))) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) by RLVECT_1:def 3
.= (L /. (x - x0)) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) by A15, VFUNCT_1:def 1
.= (L . (x - x0)) + (R /. (x - x0)) by A14, VFUNCT_1:def 1 ;
:: thesis: verum

end;

hence f1 + f2 is_differentiable_in x0 by A13, Def3; :: thesis: diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0))
hence diff ((f1 + f2),x0) = L . 1 by A13, A16, Def4
.= L /. 1 by A15, PARTFUN1:def 6
.= (L1 /. 1) + (L2 /. 1) by A15, VFUNCT_1:def 1
.= (L1 . 1) + (L2 /. 1) by A9, PARTFUN1:def 6
.= (L1 . 1) + (L2 . 1) by A9, PARTFUN1:def 6
.= (diff (f1,x0)) + (L2 . 1) by A1, A3, A5, Def4
.= (diff (f1,x0)) + (diff (f2,x0)) by A2, A6, A8, Def4 ;
:: thesis: verum