theorem Th25: :: REAL_NS3:24

for V being RealNormSpace
for W being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp W st V is finite-dimensional & dim V <> 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) holds
ex k1, k2 being Real st
( 0 < k1 & 0 < k2 & ( for x being Point of V holds
( ||.x.|| <= k1 * ((max_norm (W,b)) . x) & (max_norm (W,b)) . x <= k2 * ||.x.|| ) ) )