theorem :: REAL_NS3:25

for X, Y being RealNormSpace st RLSStruct(# the carrier of X, the ZeroF of X, the U5 of X, the Mult of X #) = RLSStruct(# the carrier of Y, the ZeroF of Y, the U5 of Y, the Mult of Y #) & X is finite-dimensional & dim X <> 0 holds
ex k1, k2 being Real st
( 0 < k1 & 0 < k2 & ( for x being Element of X
for y being Element of Y st x = y holds
( ||.x.|| <= k1 * ||.y.|| & ||.y.|| <= k2 * ||.x.|| ) ) )