let n be Nat; :: thesis: n NormF is continuous
A1: n in NAT by ORDINAL1:def 12;
for q being Point of (TOP-REAL n) holds (n NormF) . q = |.q.| by Def1;
hence n NormF is continuous by A1, JORDAN2C:83; :: thesis: verum