:: deftheorem Def3 defines Euclid_norm REAL_NS1:def 3 :
for n being Nat
for b₂ being Function of (REAL n),REAL holds
( b₂ = Euclid_norm n iff for x being Element of REAL n holds b₂ . x = |.x.| );