:: deftheorem Def1 defines NormF JGRAPH_4:def 1 :
for n being Nat
for b₂ being Function of (TOP-REAL n),R^1 holds
( b₂ = n NormF iff for q being Point of (TOP-REAL n) holds b₂ . q = |.q.| );