theorem :: NCFCONT1:59

for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for x0 being Point of CNS1 st x0 in dom f holds
f is_continuous_on {x0}