theorem Th8: :: FDIFF_2:8

for r being Real
for f being PartFunc of REAL,REAL st ex N being Neighbourhood of r st N c= dom f holds
ex h being non-zero 0 -convergent Real_Sequence ex c being constant Real_Sequence st
( rng c = {r} & rng (h + c) c= dom f & {r} c= dom f )