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