theorem Th23: :: NDIFF_4:23

for n being non zero Element of NAT
for R being PartFunc of REAL,(REAL-NS n) st R is total 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 ) ) )