theorem :: NCFCONT1:60

for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for x0 being Point of CNS st x0 in dom f holds
f is_continuous_on {x0}