let f be PartFunc of REAL,REAL; :: thesis:
let I be Interval; :: thesis:
let x be Real; :: thesis:
assume A1: f | I is_left_differentiable_in x ; :: thesis:
then consider r being Real such that
A2: ( r > 0 & [.(x - r),x.] c= dom (f | I) ) by FDIFF_3:def 4;
A3: dom (f | I) c= dom f by RELAT_1:60;
then A4: [.(x - r),x.] c= dom f by A2;
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x} & 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))) = Ldiff ((f | I),x) )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis:
let c be constant Real_Sequence; :: thesis:
assume that
A5: rng c = {x} and
A6: rng (h + c) c= dom f and
A7: for n being Nat holds h . n < 0 ; :: thesis:
consider N being Nat such that
A8: ( rng ((h ^\ N) + c) c= ].(x - r),x.[ & ( for m being Nat holds ((h ^\ N) + c) . m = (h + c) . (N + m) ) & ( for m being Nat st N <= m holds
( |.(h . m).| < r & x - r < (h + c) . m & (h + c) . m < x ) ) ) by A2, A5, A7, Lm8;
set h1 = h ^\ N;
].(x - r),x.[ c= [.(x - r),x.] by XXREAL_1:37;
then A9: rng ((h ^\ N) + c) c= dom (f | I) by A2, A8;
then A10: (f | I) /* ((h ^\ N) + c) = (f | I) * ((h ^\ N) + c) by FUNCT_2:def 11;
A11: f /* (h + c) = f * (h + c) by A6, FUNCT_2:def 11;
A12: for n being Nat holds (h ^\ N) . n < 0

proof

let n be Nat; :: thesis:
(h ^\ N) . n = h . (N + n) by NAT_1:def 3;
hence (h ^\ N) . n < 0 by A7; :: thesis:

end;

then A13: ((h ^\ N) ") (#) (((f | I) /* ((h ^\ N) + c)) - ((f | I) /* c)) is convergent by A1, A5, A9, FDIFF_3:def 4;
x - r < x by A2, XREAL_1:44;
then [.(x - r),x.] = (rng c) \/ [.(x - r),x.[ by A5, XXREAL_1:129;
then A14: rng c c= [.(x - r),x.] by XBOOLE_1:7;
then A15: rng c c= dom (f | I) by A2;
A16: rng c c= dom f by A2, A3, A14;
then A17: f /* c = f * c by FUNCT_2:def 11;
consider g being Real such that
A18: for p being Real st 0 < p holds
ex M being Nat st
for l being Nat st M <= l holds
|.(((((h ^\ N) ") (#) (((f | I) /* ((h ^\ N) + c)) - ((f | I) /* c))) . l) - g).| < p by A13, SEQ_2:def 6;
lim (((h ^\ N) ") (#) (((f | I) /* ((h ^\ N) + c)) - ((f | I) /* c))) = g by A13, A18, SEQ_2:def 7;
then A19: Ldiff ((f | I),x) = g by A1, A5, A9, A12, FDIFF_3:def 5;

A20: now :: thesis:

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider M being Nat such that
A21: for l being Nat st M <= l holds
|.(((((h ^\ N) ") (#) (((f | I) /* ((h ^\ N) + c)) - ((f | I) /* c))) . l) - g).| < p by A18;
take K = N + M; :: thesis:

hereby :: thesis:

let l be Nat; :: thesis:
assume K <= l ; :: thesis:
then reconsider i = l - (N + M) as Element of NAT by NAT_1:21;
reconsider i1 = i + M as Element of NAT by ORDINAL1:def 12;
A22: ( dom ((h ^\ N) + c) = NAT & dom c = NAT & dom (h + c) = NAT ) by FUNCT_2:def 1;
then ( i1 in dom ((h ^\ N) + c) & i1 in dom c ) ;
then ( i1 in dom ((f | I) * ((h ^\ N) + c)) & i1 in dom ((f | I) * c) ) by A9, A15, RELAT_1:27;
then i1 in (dom ((f | I) * ((h ^\ N) + c))) /\ (dom ((f | I) * c)) by XBOOLE_0:def 4;
then A23: i1 in dom (((f | I) * ((h ^\ N) + c)) - ((f | I) * c)) by VALUED_1:12;
A24: ( ((h ^\ N) + c) . i1 in rng ((h ^\ N) + c) & c . i1 in rng c ) by A22, FUNCT_1:3;
A25: ( l in dom (h + c) & l in dom c ) by A22, ORDINAL1:def 12;
then A26: c . i1 = c . l by A22, FUNCT_1:def 10;
A27: ((h ^\ N) ") . i1 = ((h ") ^\ N) . i1 by SEQM_3:18
.= (h ") . (N + i1) by NAT_1:def 3 ;
A28: ( f . ((h + c) . l) = (f * (h + c)) . l & f . (c . l) = (f * c) . l ) by A22, ORDINAL1:def 12, FUNCT_1:13;
( l in dom (f * (h + c)) & l in dom (f * c) ) by A25, A6, A16, RELAT_1:27;
then l in (dom (f /* (h + c))) /\ (dom (f /* c)) by A11, A17, XBOOLE_0:def 4;
then A29: l in dom ((f /* (h + c)) - (f /* c)) by VALUED_1:12;
(((h ^\ N) ") (#) (((f | I) /* ((h ^\ N) + c)) - ((f | I) /* c))) . i1 = (((h ^\ N) ") (#) (((f | I) * ((h ^\ N) + c)) - ((f | I) * c))) . i1 by A10, A15, FUNCT_2:def 11
.= (((h ^\ N) ") . i1) * ((((f | I) * ((h ^\ N) + c)) - ((f | I) * c)) . i1) by VALUED_1:5
.= (((h ^\ N) ") . i1) * ((((f | I) * ((h ^\ N) + c)) . i1) - (((f | I) * c) . i1)) by A23, VALUED_1:13
.= (((h ^\ N) ") . i1) * (((f | I) . (((h ^\ N) + c) . i1)) - (((f | I) * c) . i1)) by A22, FUNCT_1:13
.= (((h ^\ N) ") . i1) * (((f | I) . (((h ^\ N) + c) . i1)) - ((f | I) . (c . i1))) by A22, FUNCT_1:13
.= (((h ^\ N) ") . i1) * ((f . (((h ^\ N) + c) . i1)) - ((f | I) . (c . i1))) by A9, A24, FUNCT_1:47
.= (((h ^\ N) ") . i1) * ((f . (((h ^\ N) + c) . i1)) - (f . (c . i1))) by A2, A14, A24, FUNCT_1:47
.= ((h ") . l) * (((f * (h + c)) . l) - ((f * c) . l)) by A8, A26, A27, A28
.= ((h ") . l) * (((f /* (h + c)) - (f /* c)) . l) by A11, A17, A29, VALUED_1:13
.= ((h ") (#) ((f /* (h + c)) - (f /* c))) . l by VALUED_1:5 ;
hence |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . l) - g).| < p by A21, NAT_1:11; :: thesis:

end;

hence (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by SEQ_2:def 6; :: thesis:
hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff ((f | I),x) by A19, A20, SEQ_2:def 7; :: thesis:

end;

hence ( f is_left_differentiable_in x & Ldiff (f,x) = Ldiff ((f | I),x) ) by A2, A4, FDIFF_3:9; :: thesis: