theorem Th132: :: NCFCONT1:132

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