:: deftheorem Def7 defines diff CFDIFF_1:def 7 :
for f being PartFunc of COMPLEX,COMPLEX
for z0 being Complex st f is_differentiable_in z0 holds
for b₃ being Element of COMPLEX holds
( b₃ = diff (f,z0) iff ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( b₃ = L /. 1r & ( for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) );