let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st a < b & ].a,b.] c= dom f & f | ].a,b.] is continuous & f is_differentiable_on ].a,b.[ & f `| ].a,b.[ is_left_convergent_in b holds
( f is_left_differentiable_in b & Ldiff (f,b) = lim_left ((f `| ].a,b.[),b) )
let a, b be Real; :: thesis: ( a < b & ].a,b.] c= dom f & f | ].a,b.] is continuous & f is_differentiable_on ].a,b.[ & f `| ].a,b.[ is_left_convergent_in b implies ( f is_left_differentiable_in b & Ldiff (f,b) = lim_left ((f `| ].a,b.[),b) ) )
assume that
A1: a < b and
A2: ].a,b.] c= dom f and
A3: f | ].a,b.] is continuous and
A4: f is_differentiable_on ].a,b.[ and
A5: f `| ].a,b.[ is_left_convergent_in b ; :: thesis: ( f is_left_differentiable_in b & Ldiff (f,b) = lim_left ((f `| ].a,b.[),b) )
consider e being Real such that
A6: ( a < e & e < b ) by A1, XREAL_1:5;
[.e,b.] c= ].a,b.] by A6, XXREAL_1:39;
then A7: [.e,b.] c= dom f by A2;
set r = b - e;
e = b - (b - e) ;
then A8: ex r being Real st
( r > 0 & [.(b - r),b.] c= dom f ) by A7, A6, XREAL_1:50;
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {b} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim_left ((f `| ].a,b.[),b) )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {b} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim_left ((f `| ].a,b.[),b) )
let c be constant Real_Sequence; :: thesis: ( rng c = {b} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) implies ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim_left ((f `| ].a,b.[),b) ) )
assume that
A9: rng c = {b} and
A10: rng (h + c) c= dom f and
A11: for n being Nat holds h . n < 0 ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim_left ((f `| ].a,b.[),b) )
A12: ( h is convergent & lim h = 0 ) ;
A13: b in ].a,b.] by A1, XXREAL_1:2;
A14: dom (f `| ].a,b.[) = ].a,b.[ by A4, FDIFF_1:def 7;
A15: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_left ((f `| ].a,b.[),b))).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_left ((f `| ].a,b.[),b))).| < p )
assume A16: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_left ((f `| ].a,b.[),b))).| < p
consider R being Real such that
A17: R < b and
A18: for r1 being Real st R < r1 & r1 < b & r1 in dom (f `| ].a,b.[) holds
|.(((f `| ].a,b.[) . r1) - (lim_left ((f `| ].a,b.[),b))).| < p by A5, A16, LIMFUNC2:41;
set r = max (a,R);
A19: ( max (a,R) < b & a <= max (a,R) & R <= max (a,R) ) by A1, A17, XXREAL_0:25, XXREAL_0:29;
b - (max (a,R)) > 0 by A19, XREAL_1:50;
then consider N being Nat such that
A20: for m being Nat st N <= m holds
|.((h . m) - 0).| < b - (max (a,R)) by A12, SEQ_2:def 7;
take N ; :: thesis: for m being Nat st N <= m holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_left ((f `| ].a,b.[),b))).| < p
thus for m being Nat st N <= m holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_left ((f `| ].a,b.[),b))).| < p :: thesis: verum

proof

let m be Nat; :: thesis: ( N <= m implies |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_left ((f `| ].a,b.[),b))).| < p )
assume A21: N <= m ; :: thesis: |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_left ((f `| ].a,b.[),b))).| < p
A22: |.((h . m) - 0).| < b - (max (a,R)) by A20, A21;
h . m < 0 by A11;
then - (h . m) < b - (max (a,R)) by A22, ABSVALUE:30;
then A23: h . m > - (b - (max (a,R))) by XREAL_1:25;
A24: m in NAT by ORDINAL1:def 12;
then A25: ( m in dom (h + c) & m in dom c ) by FUNCT_2:def 1;
then c . m in rng c by FUNCT_1:3;
then A26: c . m = b by A9, TARSKI:def 1;
then A27: (h + c) . m = (h . m) + b by A25, VALUED_1:def 1;
then A28: ((max (a,R)) - b) + b < (h + c) . m by A23, XREAL_1:8;
set H = (h + c) . m;
A29: (h + c) . m < b by A11, A27, XREAL_1:30;
A30: a < (h + c) . m by A19, A28, XXREAL_0:2;
then [.((h + c) . m),b.] c= ].a,b.] by XXREAL_1:39;
then A31: [.((h + c) . m),b.] c= dom f by A2;
A32: f | [.((h + c) . m),b.] is continuous by A3, A30, FCONT_1:16, XXREAL_1:39;
A33: ].((h + c) . m),b.[ c= ].a,b.[ by A30, XXREAL_1:46;
then consider x0 being Real such that
A34: x0 in ].((h + c) . m),b.[ and
A35: diff (f,x0) = ((f . b) - (f . ((h + c) . m))) / (b - ((h + c) . m)) by A29, A31, A32, A4, FDIFF_1:26, ROLLE:3;
A36: ( (h + c) . m < x0 & x0 < b ) by A34, XXREAL_1:4;
then max (a,R) < x0 by A28, XXREAL_0:2;
then A37: R < x0 by A19, XXREAL_0:2;
A38: dom ((f /* c) - (f /* (h + c))) = NAT /\ NAT by FUNCT_2:def 1;
A39: f . ((h + c) . m) = (f /* (h + c)) . m by A10, A24, FUNCT_2:108;
f . b = (f /* c) . m by A26, A13, A24, A2, A9, ZFMISC_1:31, FUNCT_2:108;
then A40: (f . b) - (f . ((h + c) . m)) = ((f /* c) - (f /* (h + c))) . m by A39, A38, ORDINAL1:def 12, VALUED_1:13;
- (h . m) = b - ((h + c) . m) by A27;
then ((f . b) - (f . ((h + c) . m))) / (b - ((h + c) . m)) = (((f /* c) - (f /* (h + c))) . m) / ((- h) . m) by A40, VALUED_1:8;
then ((f . b) - (f . ((h + c) . m))) / (b - ((h + c) . m)) = (((f /* c) - (f /* (h + c))) /" (- h)) . m by VALUED_1:17;
then ((f . b) - (f . ((h + c) . m))) / (b - ((h + c) . m)) = (- (((f /* c) - (f /* (h + c))) /" h)) . m by SEQ_1:48;
then ((f . b) - (f . ((h + c) . m))) / (b - ((h + c) . m)) = ((- ((f /* c) - (f /* (h + c)))) /" h) . m by SEQ_1:48;
then ((f . b) - (f . ((h + c) . m))) / (b - ((h + c) . m)) = ((((- 1) (#) (f /* c)) + ((- 1) (#) (- (f /* (h + c))))) /" h) . m by SEQ_1:22;
then ((f . b) - (f . ((h + c) . m))) / (b - ((h + c) . m)) = (((- (f /* c)) + (((- 1) * (- 1)) (#) (f /* (h + c)))) /" h) . m by RFUNCT_1:17;
then ((f . b) - (f . ((h + c) . m))) / (b - ((h + c) . m)) = (((- (f /* c)) + (f /* (h + c))) /" h) . m by SEQ_1:27;
then ((h ") (#) ((f /* (h + c)) - (f /* c))) . m = (f `| ].a,b.[) . x0 by A4, A33, A34, A35, FDIFF_1:def 7;
hence |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_left ((f `| ].a,b.[),b))).| < p by A18, A36, A37, A33, A34, A14; :: thesis: verum

end;

end;

hence (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by SEQ_2:def 6; :: thesis: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim_left ((f `| ].a,b.[),b)
hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim_left ((f `| ].a,b.[),b) by A15, SEQ_2:def 7; :: thesis: verum

end;

hence ( f is_left_differentiable_in b & Ldiff (f,b) = lim_left ((f `| ].a,b.[),b) ) by A8, FDIFF_3:9; :: thesis: verum