theorem :: NCFCONT1:123

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