let V be RealNormSpace; :: thesis: ( V is finite-dimensional & dim V <> 0 implies 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).|| ) ) ) )
assume A1: ( V is finite-dimensional & dim V <> 0 ) ; :: thesis: 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).|| ) ) )
then consider S being LinearOperator of V,(REAL-NS (dim V)), W being finite-dimensional VectSp of F_Real , b being OrdBasis of W such that
A2: ( W = RLSp2RVSp V & S is bijective & ( for x being Element of W holds S . x = x |-- b ) ) by Th24;
reconsider V0 = V as finite-dimensional RealLinearSpace by A1;
reconsider b0 = b as OrdBasis of RLSp2RVSp V0 by A2;
RLSStruct(# the carrier of V0, the ZeroF of V0, the U5 of V0, the Mult of V0 #) = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ;
then consider k1, k2 being Real such that
A4: ( 0 < k1 & 0 < k2 & ( for x being Point of V holds
( ||.x.|| <= k1 * ((max_norm (V0,b0)) . x) & (max_norm (V0,b0)) . x <= k2 * ||.x.|| ) ) ) by Th25, A1;

A5: now :: thesis: for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| )

let x be Element of V; :: thesis: ( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| )
reconsider Sx = S . x as Element of REAL (dim V) by REAL_NS1:def 4;
consider x1 being Element of (RLSp2RVSp V0), z1 being Element of REAL (dim V0) such that
A6: ( x = x1 & z1 = x1 |-- b0 & (euclid_norm (V0,b0)) . x = |.z1.| ) by Def5;
A8: (euclid_norm (V0,b0)) . x = ||.(S . x).|| by A2, A6, REAL_NS1:1;
( (sum_norm (V0,b0)) . x <= (dim V) * ((max_norm (V0,b0)) . x) & (max_norm (V0,b0)) . x <= (euclid_norm (V0,b0)) . x & (euclid_norm (V0,b0)) . x <= (sum_norm (V0,b0)) . x ) by Th22, A1;
then A9: ||.(S . x).|| <= (dim V0) * ((max_norm (V0,b0)) . x) by A8, XXREAL_0:2;
(dim V0) * ((max_norm (V0,b0)) . x) <= (dim V0) * (k2 * ||.x.||) by A4, XREAL_1:64;
hence ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| by A9, XXREAL_0:2; :: thesis: ||.x.|| <= k1 * ||.(S . x).||
A10: k1 * ((max_norm (V0,b0)) . x) <= k1 * ||.(S . x).|| by A1, A4, A8, Th22, XREAL_1:64;
||.x.|| <= k1 * ((max_norm (V0,b0)) . x) by A4;
hence ||.x.|| <= k1 * ||.(S . x).|| by A10, XXREAL_0:2; :: thesis: verum

end;

set h1 = (dim V0) * k2;
take (dim V0) * k2 ; :: thesis: ex k2 being Real ex S being LinearOperator of V,(REAL-NS (dim V)) st
( S is bijective & 0 <= (dim V0) * k2 & 0 <= k2 & ( for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k2 * ||.(S . x).|| ) ) )
take k1 ; :: thesis: ex S being LinearOperator of V,(REAL-NS (dim V)) st
( S is bijective & 0 <= (dim V0) * k2 & 0 <= k1 & ( for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| ) ) )
take S ; :: thesis: ( S is bijective & 0 <= (dim V0) * k2 & 0 <= k1 & ( for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| ) ) )
thus S is bijective by A2; :: thesis: ( 0 <= (dim V0) * k2 & 0 <= k1 & ( for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| ) ) )
thus ( 0 <= (dim V0) * k2 & 0 <= k1 ) by A4; :: thesis: for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| )
thus for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| ) by A5; :: thesis: verum