let f1, f2 be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 holds
( f1 + f2 is_right_differentiable_in x0 & Rdiff ((f1 + f2),x0) = (Rdiff (f1,x0)) + (Rdiff (f2,x0)) )
let x0 be Real; :: thesis: ( f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 implies ( f1 + f2 is_right_differentiable_in x0 & Rdiff ((f1 + f2),x0) = (Rdiff (f1,x0)) + (Rdiff (f2,x0)) ) )
assume that
A1: f1 is_right_differentiable_in x0 and
A2: f2 is_right_differentiable_in x0 ; :: thesis: ( f1 + f2 is_right_differentiable_in x0 & Rdiff ((f1 + f2),x0) = (Rdiff (f1,x0)) + (Rdiff (f2,x0)) )
consider r2 being Real such that
A3: r2 > 0 and
A4: [.x0,(x0 + r2).] c= dom f2 by A2, Def3;
consider r1 being Real such that
A5: r1 > 0 and
A6: [.x0,(x0 + r1).] c= dom f1 by A1, Def3;
A7: x0 + 0 = x0 ;
set r = min (r1,r2);
0 <= min (r1,r2) by A5, A3, XXREAL_0:15;
then A8: x0 <= x0 + (min (r1,r2)) by A7, XREAL_1:9;
min (r1,r2) <= r2 by XXREAL_0:17;
then A9: x0 + (min (r1,r2)) <= x0 + r2 by XREAL_1:9;
then x0 + (min (r1,r2)) in { g where g is Real : ( x0 <= g & g <= x0 + r2 ) } by A8;
then A10: x0 + (min (r1,r2)) in [.x0,(x0 + r2).] by RCOMP_1:def 1;
x0 <= x0 + r2 by A8, A9, XXREAL_0:2;
then x0 in [.x0,(x0 + r2).] by XXREAL_1:1;
then [.x0,(x0 + (min (r1,r2))).] c= [.x0,(x0 + r2).] by A10, XXREAL_2:def 12;
then A11: [.x0,(x0 + (min (r1,r2))).] c= dom f2 by A4, XBOOLE_1:1;
min (r1,r2) <= r1 by XXREAL_0:17;
then A12: x0 + (min (r1,r2)) <= x0 + r1 by XREAL_1:9;
then x0 + (min (r1,r2)) in { g where g is Real : ( x0 <= g & g <= x0 + r1 ) } by A8;
then A13: x0 + (min (r1,r2)) in [.x0,(x0 + r1).] by RCOMP_1:def 1;
x0 <= x0 + r1 by A12, A8, XXREAL_0:2;
then x0 in [.x0,(x0 + r1).] by XXREAL_1:1;
then [.x0,(x0 + (min (r1,r2))).] c= [.x0,(x0 + r1).] by A13, XXREAL_2:def 12;
then [.x0,(x0 + (min (r1,r2))).] c= dom f1 by A6, XBOOLE_1:1;
then A14: [.x0,(x0 + (min (r1,r2))).] c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:19;
then A15: [.x0,(x0 + (min (r1,r2))).] c= dom (f1 + f2) by VALUED_1:def 1;
A16: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f1 + f2) & ( for n being Element of NAT holds h . n > 0 ) holds
( (h ") (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c)) is convergent & lim ((h ") (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c))) = (Rdiff (f1,x0)) + (Rdiff (f2,x0)) )

proof

let h be convergent_to_0 Real_Sequence; :: thesis: for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f1 + f2) & ( for n being Element of NAT holds h . n > 0 ) holds
( (h ") (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c)) is convergent & lim ((h ") (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c))) = (Rdiff (f1,x0)) + (Rdiff (f2,x0)) )
let c be V8() Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom (f1 + f2) & ( for n being Element of NAT holds h . n > 0 ) implies ( (h ") (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c)) is convergent & lim ((h ") (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c))) = (Rdiff (f1,x0)) + (Rdiff (f2,x0)) ) )
assume that
A17: rng c = {x0} and
A18: rng (h + c) c= dom (f1 + f2) and
A19: for n being Element of NAT holds h . n > 0 ; :: thesis: ( (h ") (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c)) is convergent & lim ((h ") (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c))) = (Rdiff (f1,x0)) + (Rdiff (f2,x0)) )
A20: rng (h + c) c= (dom f1) /\ (dom f2) by A18, VALUED_1:def 1;

A21: now

let n be Element of NAT ; :: thesis: (((f1 /* (h + c)) - (f1 /* c)) + ((f2 /* (h + c)) - (f2 /* c))) . n = (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c)) . n
A22: rng c c= (dom f1) /\ (dom f2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng c or x in (dom f1) /\ (dom f2) )
assume x in rng c ; :: thesis: x in (dom f1) /\ (dom f2)
then A23: x = x0 by A17, TARSKI:def 1;
x0 in [.x0,(x0 + (min (r1,r2))).] by A8, XXREAL_1:1;
hence x in (dom f1) /\ (dom f2) by A14, A23; :: thesis: verum

end;

thus (((f1 /* (h + c)) - (f1 /* c)) + ((f2 /* (h + c)) - (f2 /* c))) . n = (((f1 /* (h + c)) + (- (f1 /* c))) . n) + (((f2 /* (h + c)) - (f2 /* c)) . n) by SEQ_1:11
.= (((f1 /* (h + c)) . n) + ((- (f1 /* c)) . n)) + (((f2 /* (h + c)) + (- (f2 /* c))) . n) by SEQ_1:11
.= (((f1 /* (h + c)) . n) + ((- (f1 /* c)) . n)) + (((f2 /* (h + c)) . n) + ((- (f2 /* c)) . n)) by SEQ_1:11
.= (((f1 /* (h + c)) . n) + ((f2 /* (h + c)) . n)) + (((- (f1 /* c)) . n) + ((- (f2 /* c)) . n))
.= (((f1 /* (h + c)) . n) + ((f2 /* (h + c)) . n)) + ((- ((f1 /* c) . n)) + ((- (f2 /* c)) . n)) by SEQ_1:14
.= (((f1 /* (h + c)) . n) + ((f2 /* (h + c)) . n)) + ((- ((f1 /* c) . n)) + (- ((f2 /* c) . n))) by SEQ_1:14
.= (((f1 /* (h + c)) . n) + ((f2 /* (h + c)) . n)) - (((f1 /* c) . n) + ((f2 /* c) . n))
.= (((f1 /* (h + c)) + (f2 /* (h + c))) . n) - (((f1 /* c) . n) + ((f2 /* c) . n)) by SEQ_1:11
.= (((f1 /* (h + c)) + (f2 /* (h + c))) . n) - (((f1 /* c) + (f2 /* c)) . n) by SEQ_1:11
.= (((f1 /* (h + c)) + (f2 /* (h + c))) - ((f1 /* c) + (f2 /* c))) . n by RFUNCT_2:6
.= (((f1 + f2) /* (h + c)) - ((f1 /* c) + (f2 /* c))) . n by A20, RFUNCT_2:23
.= (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c)) . n by A22, RFUNCT_2:23 ; :: thesis: verum

end;

then A24: ((f1 /* (h + c)) - (f1 /* c)) + ((f2 /* (h + c)) - (f2 /* c)) = ((f1 + f2) /* (h + c)) - ((f1 + f2) /* c) by FUNCT_2:113;
(dom f1) /\ (dom f2) c= dom f2 by XBOOLE_1:17;
then A25: rng (h + c) c= dom f2 by A20, XBOOLE_1:1;
then A26: lim ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) = Rdiff (f2,x0) by A2, A17, A19, Th15;
Rdiff (f2,x0) = Rdiff (f2,x0) ;
then A27: (h ") (#) ((f2 /* (h + c)) - (f2 /* c)) is convergent by A2, A17, A19, A25, Th15;
(dom f1) /\ (dom f2) c= dom f1 by XBOOLE_1:17;
then A28: rng (h + c) c= dom f1 by A20, XBOOLE_1:1;
A29: ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) + ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) = (h ") (#) (((f1 /* (h + c)) - (f1 /* c)) + ((f2 /* (h + c)) - (f2 /* c))) by SEQ_1:24;
Rdiff (f1,x0) = Rdiff (f1,x0) ;
then A30: (h ") (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent by A1, A17, A19, A28, Th15;
then ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) + ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A27, SEQ_2:19;
hence (h ") (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c)) is convergent by A29, A21, FUNCT_2:113; :: thesis: lim ((h ") (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c))) = (Rdiff (f1,x0)) + (Rdiff (f2,x0))
lim ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) = Rdiff (f1,x0) by A1, A17, A19, A28, Th15;
hence lim ((h ") (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c))) = (Rdiff (f1,x0)) + (Rdiff (f2,x0)) by A30, A27, A26, A29, A24, SEQ_2:20; :: thesis: verum

end;

0 < min (r1,r2) by A5, A3, XXREAL_0:15;
hence ( f1 + f2 is_right_differentiable_in x0 & Rdiff ((f1 + f2),x0) = (Rdiff (f1,x0)) + (Rdiff (f2,x0)) ) by A15, A16, Th15; :: thesis: verum