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 that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_left_differentiable_in x0 ; :: thesis: ( f1 - f2 is_left_differentiable_in x0 & Ldiff ((f1 - f2),x0) = (Ldiff (f1,x0)) - (Ldiff (f2,x0)) )
consider r2 being Real such that
A3: 0 < r2 and
A4: [.(x0 - r2),x0.] c= dom f2 by A2;
consider r1 being Real such that
A5: 0 < r1 and
A6: [.(x0 - r1),x0.] c= dom f1 by A1;
set r = min (r1,r2);
A7: 0 < min (r1,r2) by A5, A3, XXREAL_0:15;
then A8: x0 - (min (r1,r2)) <= x0 by XREAL_1:43;
min (r1,r2) <= r2 by XXREAL_0:17;
then A9: x0 - r2 <= x0 - (min (r1,r2)) by XREAL_1:13;
then x0 - r2 <= x0 by A8, XXREAL_0:2;
then A10: x0 in [.(x0 - r2),x0.] by XXREAL_1:1;
x0 - (min (r1,r2)) in { g where g is Real : ( x0 - r2 <= g & g <= x0 ) } by A8, A9;
then x0 - (min (r1,r2)) in [.(x0 - r2),x0.] by RCOMP_1:def 1;
then [.(x0 - (min (r1,r2))),x0.] c= [.(x0 - r2),x0.] by A10, XXREAL_2:def 12;
then A11: [.(x0 - (min (r1,r2))),x0.] c= dom f2 by A4;
min (r1,r2) <= r1 by XXREAL_0:17;
then A12: x0 - r1 <= x0 - (min (r1,r2)) by XREAL_1:13;
then x0 - r1 <= x0 by A8, XXREAL_0:2;
then A13: x0 in [.(x0 - r1),x0.] by XXREAL_1:1;
x0 - (min (r1,r2)) in { g where g is Real : ( x0 - r1 <= g & g <= x0 ) } by A8, A12;
then x0 - (min (r1,r2)) in [.(x0 - r1),x0.] by RCOMP_1:def 1;
then [.(x0 - (min (r1,r2))),x0.] c= [.(x0 - r1),x0.] by A13, XXREAL_2:def 12;
then [.(x0 - (min (r1,r2))),x0.] c= dom f1 by A6;
then A14: [.(x0 - (min (r1,r2))),x0.] c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:19;
A15: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f1 - f2) & ( for n being 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 non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f1 - f2) & ( for n being 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 constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom (f1 - f2) & ( for n being 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
A16: rng c = {x0} and
A17: rng (h + c) c= dom (f1 - f2) and
A18: for n being 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)) )
A19: rng (h + c) c= (dom f1) /\ (dom f2) by A17, VALUED_1:12;
A20: now :: thesis: for n being Element of NAT holds (((f1 /* (h + c)) - (f1 /* c)) - ((f2 /* (h + c)) - (f2 /* c))) . n = (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c)) . n
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
A21: rng c c= (dom f1) /\ (dom f2)
proof
let x be object ; :: 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 A22: x = x0 by A16, TARSKI:def 1;
x0 in [.(x0 - (min (r1,r2))),x0.] by A8, XXREAL_1:1;
hence x in (dom f1) /\ (dom f2) by A14, A22; :: 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:1
.= (((f1 /* (h + c)) . n) - ((f1 /* c) . n)) - (((f2 /* (h + c)) - (f2 /* c)) . n) by RFUNCT_2:1
.= (((f1 /* (h + c)) . n) - ((f1 /* c) . n)) - (((f2 /* (h + c)) . n) - ((f2 /* c) . n)) by RFUNCT_2:1
.= (((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:1
.= (((f1 /* (h + c)) - (f2 /* (h + c))) . n) - (((f1 /* c) - (f2 /* c)) . n) by RFUNCT_2:1
.= (((f1 /* (h + c)) - (f2 /* (h + c))) - ((f1 /* c) - (f2 /* c))) . n by RFUNCT_2:1
.= (((f1 - f2) /* (h + c)) - ((f1 /* c) - (f2 /* c))) . n by A19, RFUNCT_2:8
.= (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c)) . n by A21, RFUNCT_2:8 ; :: thesis: verum
end;
then A23: ((f1 /* (h + c)) - (f1 /* c)) - ((f2 /* (h + c)) - (f2 /* c)) = ((f1 - f2) /* (h + c)) - ((f1 - f2) /* c) by FUNCT_2:63;
(dom f1) /\ (dom f2) c= dom f2 by XBOOLE_1:17;
then A24: rng (h + c) c= dom f2 by A19;
then A25: lim ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) = Ldiff (f2,x0) by A2, A16, A18, Th9;
A26: (h ") (#) ((f2 /* (h + c)) - (f2 /* c)) is convergent by A2, A16, A18, A24;
(dom f1) /\ (dom f2) c= dom f1 by XBOOLE_1:17;
then A27: rng (h + c) c= dom f1 by A19;
A28: ((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:21;
A29: (h ") (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent by A1, A16, A18, A27;
then ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) - ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A26;
hence (h ") (#) (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c)) is convergent by A28, A20, FUNCT_2:63; :: thesis: lim ((h ") (#) (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c))) = (Ldiff (f1,x0)) - (Ldiff (f2,x0))
lim ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) = Ldiff (f1,x0) by A1, A16, A18, A27, Th9;
hence lim ((h ") (#) (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c))) = (Ldiff (f1,x0)) - (Ldiff (f2,x0)) by A29, A26, A25, A28, A23, SEQ_2:12; :: thesis: verum
end;
[.(x0 - (min (r1,r2))),x0.] c= dom (f1 - f2) by A14, VALUED_1:12;
hence ( f1 - f2 is_left_differentiable_in x0 & Ldiff ((f1 - f2),x0) = (Ldiff (f1,x0)) - (Ldiff (f2,x0)) ) by A7, A15, Th9; :: thesis: verum