theorem Th1: :: NDIFF_5:1

for S being RealNormSpace
for R being Function of REAL,S 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
(|.z.| ") * ||.(R /. z).|| < r ) ) )