theorem Th17: :: NDIFF_5:17

for T being RealNormSpace
for R being PartFunc of REAL,T 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
||.(R /. z).|| / |.z.| < r ) ) )