theorem Th35: :: ORDEQ_01:35

for R being PartFunc of REAL,REAL 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 ) ) )