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