theorem Th128: :: NCFCONT1:128

for CNS being ComplexNormSpace
for f being PartFunc of CNS,CNS st ( for x0 being Point of CNS st x0 in dom f holds
f /. x0 = x0 ) holds
f is_continuous_on dom f