for x0 being Complex
for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_in x0 holds
ex R being C_RestFunc st
( R /. 0c = 0c & R is_continuous_in 0c )