theorem Th2: :: NDIFF_5:2

for S being RealNormSpace
for R being RestFunc of S st R /. 0 = 0. S holds
for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) )