let X, Y be RealNormSpace; ( 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 implies 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.|| ) ) ) )
assume A1:
( 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 )
; 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.|| ) ) )
set X0 = (Omega). X;
set Y0 = (Omega). Y;
A2:
(Omega). X = RLSStruct(# the carrier of X, the ZeroF of X, the U5 of X, the Mult of X #)
by RLSUB_1:def 4;
reconsider X0 = (Omega). X as finite-dimensional RealLinearSpace by A1;
A3:
dim X = dim X0
by A1, RLVECT_5:30;
(Omega). Y = RLSStruct(# the carrier of Y, the ZeroF of Y, the U5 of Y, the Mult of Y #)
by RLSUB_1:def 4;
then A4:
Y is finite-dimensional
by A1, RLAFFIN3:3, A2;
reconsider Y0 = (Omega). Y as finite-dimensional RealLinearSpace by A1, A2, RLSUB_1:def 4;
X0 = Y0
by A1, A2, RLSUB_1:def 4;
then A6:
dim X = dim Y
by A3, A4, RLVECT_5:30;
set b = the OrdBasis of RLSp2RVSp X0;
reconsider e = the OrdBasis of RLSp2RVSp X0 as OrdBasis of RLSp2RVSp Y0 by A1, A2, RLSUB_1:def 4;
consider k1, k2 being Real such that
A7:
( 0 < k1 & 0 < k2 & ( for x being Point of X holds
( ||.x.|| <= k1 * ((max_norm (X0, the OrdBasis of RLSp2RVSp X0)) . x) & (max_norm (X0, the OrdBasis of RLSp2RVSp X0)) . x <= k2 * ||.x.|| ) ) )
by A1, A2, Th25;
Y0 = RLSStruct(# the carrier of Y, the ZeroF of Y, the U5 of Y, the Mult of Y #)
by RLSUB_1:def 4;
then consider j1, j2 being Real such that
A8:
( 0 < j1 & 0 < j2 & ( for x being Point of Y holds
( ||.x.|| <= j1 * ((max_norm (Y0,e)) . x) & (max_norm (Y0,e)) . x <= j2 * ||.x.|| ) ) )
by A1, A4, A6, Th25;
A9:
now for x being Element of X
for y being Element of Y st x = y holds
( ||.x.|| <= (k1 * j2) * ||.y.|| & ||.y.|| <= (j1 * k2) * ||.x.|| )let x be
Element of
X;
for y being Element of Y st x = y holds
( ||.x.|| <= (k1 * j2) * ||.y.|| & ||.y.|| <= (j1 * k2) * ||.x.|| )let y be
Element of
Y;
( x = y implies ( ||.x.|| <= (k1 * j2) * ||.y.|| & ||.y.|| <= (j1 * k2) * ||.x.|| ) )assume
x = y
;
( ||.x.|| <= (k1 * j2) * ||.y.|| & ||.y.|| <= (j1 * k2) * ||.x.|| )then A12:
(max_norm (X0, the OrdBasis of RLSp2RVSp X0)) . x = (max_norm (Y0,e)) . y
by A1, A2, RLSUB_1:def 4;
A11:
(
||.x.|| <= k1 * ((max_norm (X0, the OrdBasis of RLSp2RVSp X0)) . x) &
(max_norm (X0, the OrdBasis of RLSp2RVSp X0)) . x <= k2 * ||.x.|| &
||.y.|| <= j1 * ((max_norm (Y0,e)) . y) &
(max_norm (Y0,e)) . y <= j2 * ||.y.|| )
by A7, A8;
k1 * ((max_norm (Y0,e)) . y) <= k1 * (j2 * ||.y.||)
by A7, A8, XREAL_1:64;
hence
||.x.|| <= (k1 * j2) * ||.y.||
by A11, A12, XXREAL_0:2;
||.y.|| <= (j1 * k2) * ||.x.||
j1 * ((max_norm (X0, the OrdBasis of RLSp2RVSp X0)) . x) <= j1 * (k2 * ||.x.||)
by A7, A8, XREAL_1:64;
hence
||.y.|| <= (j1 * k2) * ||.x.||
by A11, A12, XXREAL_0:2;
verum end;
set h1 = k1 * j2;
set h2 = j1 * k2;
take
k1 * j2
; ex k2 being Real st
( 0 < k1 * j2 & 0 < k2 & ( for x being Element of X
for y being Element of Y st x = y holds
( ||.x.|| <= (k1 * j2) * ||.y.|| & ||.y.|| <= k2 * ||.x.|| ) ) )
take
j1 * k2
; ( 0 < k1 * j2 & 0 < j1 * k2 & ( for x being Element of X
for y being Element of Y st x = y holds
( ||.x.|| <= (k1 * j2) * ||.y.|| & ||.y.|| <= (j1 * k2) * ||.x.|| ) ) )
thus
( 0 < k1 * j2 & 0 < j1 * k2 )
by A7, A8, XREAL_1:129; for x being Element of X
for y being Element of Y st x = y holds
( ||.x.|| <= (k1 * j2) * ||.y.|| & ||.y.|| <= (j1 * k2) * ||.x.|| )
thus
for x being Element of X
for y being Element of Y st x = y holds
( ||.x.|| <= (k1 * j2) * ||.y.|| & ||.y.|| <= (j1 * k2) * ||.x.|| )
by A9; verum