:: deftheorem Def1 defines distance_by_norm_of NORMSP_2:def 1 :
for X being RealNormSpace
for b₂ being Function of [: the carrier of X, the carrier of X:],REAL holds
( b₂ = distance_by_norm_of X iff for x, y being Point of X holds b₂ . (x,y) = ||.(x - y).|| );