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