theorem Th27: :: REAL_NS3:26

for V being RealNormSpace st V is finite-dimensional & dim V <> 0 holds
ex k1, k2 being Real ex S being LinearOperator of V,(REAL-NS (dim V)) st
( S is bijective & 0 <= k1 & 0 <= k2 & ( for x being Element of V holds
( ||.(S . x).|| <= k1 * ||.x.|| & ||.x.|| <= k2 * ||.(S . x).|| ) ) )