let f1, f2 be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval st I c= dom (f1 + f2) & f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval I holds
( f1 + f2 is_differentiable_on_interval I & (f1 + f2) `\ I = (f1 `\ I) + (f2 `\ I) & ( for x being Real st x in I holds
((f1 + f2) `\ I) . x = ((f1 `\ I) . x) + ((f2 `\ I) . x) ) )
let I be non empty Interval; :: thesis: ( I c= dom (f1 + f2) & f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval I implies ( f1 + f2 is_differentiable_on_interval I & (f1 + f2) `\ I = (f1 `\ I) + (f2 `\ I) & ( for x being Real st x in I holds
((f1 + f2) `\ I) . x = ((f1 `\ I) . x) + ((f2 `\ I) . x) ) ) )
assume that
A1: I c= dom (f1 + f2) and
A2: f1 is_differentiable_on_interval I and
A3: f2 is_differentiable_on_interval I ; :: thesis: ( f1 + f2 is_differentiable_on_interval I & (f1 + f2) `\ I = (f1 `\ I) + (f2 `\ I) & ( for x being Real st x in I holds
((f1 + f2) `\ I) . x = ((f1 `\ I) . x) + ((f2 `\ I) . x) ) )
set J = ].(inf I),(sup I).[;
].(inf I),(sup I).[ c= I by Lm13;
then A4: ].(inf I),(sup I).[ c= dom (f1 + f2) by A1;
A5: for x being Real st x in ].(inf I),(sup I).[ holds
(f1 + f2) | ].(inf I),(sup I).[ is_differentiable_in x

proof

let x be Real; :: thesis: ( x in ].(inf I),(sup I).[ implies (f1 + f2) | ].(inf I),(sup I).[ is_differentiable_in x )
assume x in ].(inf I),(sup I).[ ; :: thesis: (f1 + f2) | ].(inf I),(sup I).[ is_differentiable_in x
then ( f1 | ].(inf I),(sup I).[ is_differentiable_in x & f2 | ].(inf I),(sup I).[ is_differentiable_in x ) by A2, A3, FDIFF_1:def 6;
then (f1 | ].(inf I),(sup I).[) + (f2 | ].(inf I),(sup I).[) is_differentiable_in x by FDIFF_1:13;
hence (f1 + f2) | ].(inf I),(sup I).[ is_differentiable_in x by RFUNCT_1:44; :: thesis: verum

end;

hence A6: f1 + f2 is_differentiable_on_interval I by A1, A2, A3, A4, FDIFF_1:def 6, FDIFF_3:10, FDIFF_3:16; :: thesis: ( (f1 + f2) `\ I = (f1 `\ I) + (f2 `\ I) & ( for x being Real st x in I holds
((f1 + f2) `\ I) . x = ((f1 `\ I) . x) + ((f2 `\ I) . x) ) )
then A7: dom ((f1 + f2) `\ I) = I by Def2;
( dom (f1 `\ I) = I & dom (f2 `\ I) = I ) by A2, A3, Def2;
then A8: dom ((f1 `\ I) + (f2 `\ I)) = I /\ I by VALUED_1:def 1;
A9: for x being Element of REAL st x in dom ((f1 + f2) `\ I) holds
((f1 + f2) `\ I) . x = ((f1 `\ I) + (f2 `\ I)) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom ((f1 + f2) `\ I) implies ((f1 + f2) `\ I) . x = ((f1 `\ I) + (f2 `\ I)) . x )
assume A10: x in dom ((f1 + f2) `\ I) ; :: thesis: ((f1 + f2) `\ I) . x = ((f1 `\ I) + (f2 `\ I)) . x
then A11: x in I by A6, Def2;

per cases ( x = inf I or x = sup I or ( x <> inf I & x <> sup I ) ) ;

suppose A12: x = inf I ; :: thesis: ((f1 + f2) `\ I) . x = ((f1 `\ I) + (f2 `\ I)) . x

then A13: inf I = lower_bound I by A11, Lm5;
( (f1 `\ I) . x = Rdiff (f1,x) & (f2 `\ I) . x = Rdiff (f2,x) & ((f1 + f2) `\ I) . x = Rdiff ((f1 + f2),x) ) by A2, A3, A6, A11, A12, Def2;
then ((f1 + f2) `\ I) . x = ((f1 `\ I) . x) + ((f2 `\ I) . x) by A10, A6, Def2, A12, A13, A2, A3, FDIFF_3:16;
hence ((f1 + f2) `\ I) . x = ((f1 `\ I) + (f2 `\ I)) . x by A7, A8, A10, VALUED_1:def 1; :: thesis: verum

end;

suppose A14: x = sup I ; :: thesis: ((f1 + f2) `\ I) . x = ((f1 `\ I) + (f2 `\ I)) . x

then A15: sup I = upper_bound I by A11, Lm6;
( (f1 `\ I) . x = Ldiff (f1,x) & (f2 `\ I) . x = Ldiff (f2,x) & ((f1 + f2) `\ I) . x = Ldiff ((f1 + f2),x) ) by A2, A3, A6, A11, A14, Def2;
then ((f1 + f2) `\ I) . x = ((f1 `\ I) . x) + ((f2 `\ I) . x) by A10, A6, Def2, A14, A15, A2, A3, FDIFF_3:10;
hence ((f1 + f2) `\ I) . x = ((f1 `\ I) + (f2 `\ I)) . x by A7, A8, A10, VALUED_1:def 1; :: thesis: verum

end;

suppose A16: ( x <> inf I & x <> sup I ) ; :: thesis: ((f1 + f2) `\ I) . x = ((f1 `\ I) + (f2 `\ I)) . x

A17: ( (f1 `\ I) . x = diff (f1,x) & (f2 `\ I) . x = diff (f2,x) & ((f1 + f2) `\ I) . x = diff ((f1 + f2),x) ) by A16, A11, A2, A3, A6, Def2;
( inf I <= x & x <= sup I ) by A11, XXREAL_2:61, XXREAL_2:62;
then A18: ( inf I < x & x < sup I ) by A16, XXREAL_0:1;
consider Z being open Subset of REAL such that
A19: ( x in Z & Z c= ].(inf I),(sup I).[ ) by A18, Lm9;
A20: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z & f1 + f2 is_differentiable_on Z ) by A2, A3, A5, A19, A4, FDIFF_1:def 6, FDIFF_1:26;
then ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) by A19, FDIFF_1:18;
then ((f1 + f2) `\ I) . x = ((f1 `\ I) . x) + ((f2 `\ I) . x) by A17, A19, A20, FDIFF_1:def 7;
hence ((f1 + f2) `\ I) . x = ((f1 `\ I) + (f2 `\ I)) . x by A7, A8, A10, VALUED_1:def 1; :: thesis: verum

end;

end;

end;

hence (f1 + f2) `\ I = (f1 `\ I) + (f2 `\ I) by A7, A8, PARTFUN1:5; :: thesis: for x being Real st x in I holds
((f1 + f2) `\ I) . x = ((f1 `\ I) . x) + ((f2 `\ I) . x)

hereby :: thesis: verum

let x be Real; :: thesis: ( x in I implies ((f1 + f2) `\ I) . x = ((f1 `\ I) . x) + ((f2 `\ I) . x) )
assume A21: x in I ; :: thesis: ((f1 + f2) `\ I) . x = ((f1 `\ I) . x) + ((f2 `\ I) . x)
then ((f1 + f2) `\ I) . x = ((f1 `\ I) + (f2 `\ I)) . x by A7, A9;
hence ((f1 + f2) `\ I) . x = ((f1 `\ I) . x) + ((f2 `\ I) . x) by A21, A8, VALUED_1:def 1; :: thesis: verum

end;