theorem :: NCFCONT1:61

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