theorem :: NCFCONT1:122

for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st ex r being Point of CNS2 st rng f = {r} holds
f is_continuous_on dom f