theorem Th18: :: NDIFF_5:18
for R being Function of REAL,REAL holds
( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
|.(R . z).| / |.z.| < r ) ) )