theorem :: CFCONT_1:42

for x0 being Complex
for f being PartFunc of COMPLEX,COMPLEX st x0 in dom f holds
f is_continuous_on {x0}