:: deftheorem Def1 defines RestFunc-like NDIFF_3:def 1 :
for F being RealNormSpace
for IT being PartFunc of REAL, the carrier of F holds
( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0. F ) ) ) );