theorem Th1: :: FDIFF_3:1

for f being PartFunc of REAL,REAL
for x0 being Real st ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom f ) holds
ex h being non-zero 0 -convergent Real_Sequence ex c being constant Real_Sequence st
( rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) )