:: deftheorem Def5 defines euclid_norm REAL_NS3:def 5 :
for X being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp X
for b₃ being Function of X,REAL holds
( b₃ = euclid_norm (X,b) iff for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & b₃ . x = |.z.| ) );