theorem :: CFCONT_1:35
for x0 being Complex
for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 holds
- f is_continuous_in x0 by Th34;