theorem Th9: :: FDIFF_3:9

for f being PartFunc of REAL,REAL
for x0, g being Real holds
( f is_left_differentiable_in x0 & Ldiff (f,x0) = g iff ( ex r being Real st
( 0 < r & [.(x0 - r),x0.] c= dom f ) & ( 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
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = g ) ) ) )