let f1, f2 be PartFunc of REAL , REAL ; :: thesis: for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 holds
( f1 - f2 is_left_differentiable_in x0 & Ldiff (f1 - f2),x0 = (Ldiff f1,x0) - (Ldiff f2,x0) )
let x0 be Real; :: thesis: ( f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 implies ( f1 - f2 is_left_differentiable_in x0 & Ldiff (f1 - f2),x0 = (Ldiff f1,x0) - (Ldiff f2,x0) ) )
assume A1: ( f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 ) ; :: thesis: ( f1 - f2 is_left_differentiable_in x0 & Ldiff (f1 - f2),x0 = (Ldiff f1,x0) - (Ldiff f2,x0) )
then consider r1 being Real such that
A2: ( 0 < r1 & [.(x0 - r1),x0.] c= dom f1 ) by Def4;
consider r2 being Real such that
A3: ( 0 < r2 & [.(x0 - r2),x0.] c= dom f2 ) by A1, Def4;
set r = min r1,r2;
A4: 0 < min r1,r2 by A2, A3, XXREAL_0:15;
then A5: x0 - (min r1,r2) <= x0 by XREAL_1:45;
min r1,r2 <= r1 by XXREAL_0:17;
then A6: x0 - r1 <= x0 - (min r1,r2) by XREAL_1:15;
then x0 - (min r1,r2) in { g where g is Real : ( x0 - r1 <= g & g <= x0 ) } by A5;
then A7: x0 - (min r1,r2) in [.(x0 - r1),x0.] by RCOMP_1:def 1;
x0 - r1 <= x0 by A5, A6, XXREAL_0:2;
then x0 in [.(x0 - r1),x0.] by XXREAL_1:1;
then A8: [.(x0 - (min r1,r2)),x0.] c= [.(x0 - r1),x0.] by A7, XXREAL_2:def 12;
min r1,r2 <= r2 by XXREAL_0:17;
then A9: x0 - r2 <= x0 - (min r1,r2) by XREAL_1:15;
then x0 - (min r1,r2) in { g where g is Real : ( x0 - r2 <= g & g <= x0 ) } by A5;
then A10: x0 - (min r1,r2) in [.(x0 - r2),x0.] by RCOMP_1:def 1;
x0 - r2 <= x0 by A5, A9, XXREAL_0:2;
then x0 in [.(x0 - r2),x0.] by XXREAL_1:1;
then A11: [.(x0 - (min r1,r2)),x0.] c= [.(x0 - r2),x0.] by A10, XXREAL_2:def 12;
A12: [.(x0 - (min r1,r2)),x0.] c= dom f1 by A2, A8, XBOOLE_1:1;
[.(x0 - (min r1,r2)),x0.] c= dom f2 by A3, A11, XBOOLE_1:1;
then A13: [.(x0 - (min r1,r2)),x0.] c= (dom f1) /\ (dom f2) by A12, XBOOLE_1:19;
then A14: [.(x0 - (min r1,r2)),x0.] c= dom (f1 - f2) by VALUED_1:12;
for h being convergent_to_0 Real_Sequence
for c being V6 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))) = (Ldiff f1,x0) - (Ldiff f2,x0) )

proof

let h be convergent_to_0 Real_Sequence; :: thesis: for c being V6 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))) = (Ldiff f1,x0) - (Ldiff f2,x0) )
let c be V6 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))) = (Ldiff f1,x0) - (Ldiff f2,x0) ) )
assume that
A15: rng c = {x0} and
A16: rng (h + c) c= dom (f1 - f2) and
A17: 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))) = (Ldiff f1,x0) - (Ldiff f2,x0) )
A18: rng (h + c) c= (dom f1) /\ (dom f2) by A16, VALUED_1:12;
( (dom f1) /\ (dom f2) c= dom f1 & (dom f1) /\ (dom f2) c= dom f2 ) by XBOOLE_1:17;
then A19: ( rng (h + c) c= dom f1 & rng (h + c) c= dom f2 ) by A18, XBOOLE_1:1;
Ldiff f1,x0 = Ldiff f1,x0 ;
then A20: ( (h " ) (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent & lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) = Ldiff f1,x0 ) by A1, A15, A17, A19, Th9;
Ldiff f2,x0 = Ldiff f2,x0 ;
then A21: ( (h " ) (#) ((f2 /* (h + c)) - (f2 /* c)) is convergent & lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) = Ldiff f2,x0 ) by A1, A15, A17, A19, Th9;
then A22: ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) - ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A20, SEQ_2:25;
A23: ((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:29;

A24: 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
A25: 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 A26: x = x0 by A15, TARSKI:def 1;
x0 in [.(x0 - (min r1,r2)),x0.] by A5, XXREAL_1:1;
hence x in (dom f1) /\ (dom f2) by A13, A26; :: 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 RFUNCT_2:6
.= (((f1 /* (h + c)) . n) - ((f1 /* c) . n)) - (((f2 /* (h + c)) - (f2 /* c)) . n) by RFUNCT_2:6
.= (((f1 /* (h + c)) . n) - ((f1 /* c) . n)) - (((f2 /* (h + c)) . n) - ((f2 /* c) . n)) by RFUNCT_2:6
.= (((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 RFUNCT_2:6
.= (((f1 /* (h + c)) - (f2 /* (h + c))) . n) - (((f1 /* c) - (f2 /* c)) . n) by RFUNCT_2:6
.= (((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 A18, RFUNCT_2:23
.= (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c)) . n by A25, RFUNCT_2:23 ; :: thesis: verum

end;

then A27: ((f1 /* (h + c)) - (f1 /* c)) - ((f2 /* (h + c)) - (f2 /* c)) = ((f1 - f2) /* (h + c)) - ((f1 - f2) /* c) by FUNCT_2:113;
thus (h " ) (#) (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c)) is convergent by A22, A23, A24, FUNCT_2:113; :: thesis: lim ((h " ) (#) (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c))) = (Ldiff f1,x0) - (Ldiff f2,x0)
thus lim ((h " ) (#) (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c))) = (Ldiff f1,x0) - (Ldiff f2,x0) by A20, A21, A23, A27, SEQ_2:26; :: thesis: verum

end;

hence ( f1 - f2 is_left_differentiable_in x0 & Ldiff (f1 - f2),x0 = (Ldiff f1,x0) - (Ldiff f2,x0) ) by A4, A14, Th9; :: thesis: verum