:: deftheorem Def8 defines RLMSpace VECTMETR:def 8 :
for n being Element of NAT
for b₂ being strict RealLinearMetrSpace holds
( b₂ = RLMSpace n iff ( the carrier of b₂ = REAL n & the distance of b₂ = Pitag_dist n & 0. b₂ = 0* n & ( for x, y being Element of REAL n holds the addF of b₂ . (x,y) = x + y ) & ( for x being Element of REAL n
for r being Element of REAL holds the Mult of b₂ . (r,x) = r * x ) ) );