:: deftheorem Def2 defines RestFunc-like FDIFF_1:def 2 :
for IT being PartFunc of REAL,REAL 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 ) ) ) );