theorem :: NCFCONT1:124

for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS st ex r being Point of CNS st rng f = {r} holds
f is_continuous_on dom f