:: deftheorem Def5 defines RestFunc-like NDIFF_1:def 5 :
for S, T being RealNormSpace
for IT being PartFunc of S,T holds
( IT is RestFunc-like iff ( IT is total & ( for h being 0. b₁ -convergent sequence of S st h is non-zero holds
( (||.h.|| ") (#) (IT /* h) is convergent & lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) ) );