:: deftheorem Def3 defines RestFunc-like CFDIFF_1:def 3 :
for IT being PartFunc of COMPLEX,COMPLEX holds
( IT is RestFunc-like iff for h being non-zero 0 -convergent Complex_Sequence holds
( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ) );