:: deftheorem Def1 defines normRU DUALSP04:def 1 :
for X being RealUnitarySpace
for b₂ being Function of the carrier of X,REAL holds
( b₂ = normRU X iff for x being Point of X holds b₂ . x = ||.x.|| );