let V be finite-dimensional RealNormSpace; :: thesis: ( dim V <> 0 implies ex L being LinearOperator of V,(REAL-NS (dim V)) st
( L is one-to-one & L is onto & L is isometric-like ) )
assume dim V <> 0 ; :: thesis: ex L being LinearOperator of V,(REAL-NS (dim V)) st
( L is one-to-one & L is onto & L is isometric-like )
then consider k1, k2 being Real, S being LinearOperator of V,(REAL-NS (dim V)) such that
A1: ( S is bijective & 0 <= k1 & 0 <= k2 & ( for x being Element of V holds
( ||.(S . x).|| <= k1 * ||.x.|| & ||.x.|| <= k2 * ||.(S . x).|| ) ) ) by Th27;
take S ; :: thesis: ( S is one-to-one & S is onto & S is isometric-like )
thus ( S is one-to-one & S is onto ) by A1; :: thesis: S is isometric-like
thus S is isometric-like by A1; :: thesis: verum