let V be torsion-free Z_Module; for r being Element of F_Rat st r <> 0. F_Rat holds
ex T being linear-transformation of (EMbedding V),(EMbedding (r,V)) st
( ( for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds
T . v = r * v ) & T is bijective )
let r be Element of F_Rat; ( r <> 0. F_Rat implies ex T being linear-transformation of (EMbedding V),(EMbedding (r,V)) st
( ( for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds
T . v = r * v ) & T is bijective ) )
assume AS:
r <> 0. F_Rat
; ex T being linear-transformation of (EMbedding V),(EMbedding (r,V)) st
( ( for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds
T . v = r * v ) & T is bijective )
set EZV = Z_MQ_VectSp V;
deffunc H1( Vector of (Z_MQ_VectSp V)) -> Element of the carrier of (Z_MQ_VectSp V) = r * $1;
consider T being Function of the carrier of (Z_MQ_VectSp V), the carrier of (Z_MQ_VectSp V) such that
P1:
for x being Element of the carrier of (Z_MQ_VectSp V) holds T . x = H1(x)
from FUNCT_2:sch 4();
set T0 = T | the carrier of (EMbedding V);
D0:
the carrier of (EMbedding V) = rng (MorphsZQ V)
by defEmbedding;
dom T = the carrier of (Z_MQ_VectSp V)
by FUNCT_2:def 1;
then P3:
dom (T | the carrier of (EMbedding V)) = the carrier of (EMbedding V)
by D0, RELAT_1:62;
D1:
the carrier of (EMbedding (r,V)) = r * (rng (MorphsZQ V))
by defriV;
RX0:
for y being object holds
( y in rng (T | the carrier of (EMbedding V)) iff y in the carrier of (EMbedding (r,V)) )
then
rng (T | the carrier of (EMbedding V)) = the carrier of (EMbedding (r,V))
by TARSKI:2;
then reconsider T0 = T | the carrier of (EMbedding V) as Function of (EMbedding V),(EMbedding (r,V)) by P3, FUNCT_2:1;
B0:
T0 is additive
for x being Element of (EMbedding V)
for i being Element of INT.Ring holds T0 . (i * x) = i * (T0 . x)
then
( T0 is additive & T0 is homogeneous )
by B0;
then reconsider T0 = T0 as linear-transformation of (EMbedding V),(EMbedding (r,V)) ;
take
T0
; ( ( for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds
T0 . v = r * v ) & T0 is bijective )
thus XX1:
for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds
T0 . v = r * v
T0 is bijective
for x1, x2 being object st x1 in the carrier of (EMbedding V) & x2 in the carrier of (EMbedding V) & T0 . x1 = T0 . x2 holds
x1 = x2
then T1:
T0 is one-to-one
by FUNCT_2:19;
T0 is onto
by RX0, FUNCT_2:def 3, TARSKI:2;
hence
T0 is bijective
by T1; verum