:: deftheorem Def5 defines Ldiff FDIFF_3:def 5 :
for x0 being Real
for f being PartFunc of REAL,REAL st f is_left_differentiable_in x0 holds
for b₃ being Real holds
( b₃ = Ldiff (f,x0) iff for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds
b₃ = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) );