for n being Element of NAT
for K0 being Subset of (TOP-REAL n)
for f being Function of ((TOP-REAL n) | K0),R^1 st ( for p being Point of ((TOP-REAL n) | K0) holds f . p = (n NormF) . p ) holds
f is continuous