let V be torsion-free Z_Module; :: thesis: ex T being linear-transformation of V,(EMbedding V) st
( T is bijective & T = MorphsZQ V & ( for v being Vector of V holds T . v = Class ((EQRZM V),[v,1]) ) )
set T = MorphsZQ V;
rng (MorphsZQ V) = the carrier of (EMbedding V) by defEmbedding;
then reconsider T0 = MorphsZQ V as Function of V,(EMbedding V) by FUNCT_2:6;
B0: T0 is additive

proof

let x, y be Element of V; :: according to VECTSP_1:def 19 :: thesis: T0 . (x + y) = (T0 . x) + (T0 . y)
thus T0 . (x + y) = (T0 . x) + (T0 . y) :: thesis: verum

proof

L1: (MorphsZQ V) . (x + y) = ((MorphsZQ V) . x) + ((MorphsZQ V) . y) by ZMODUL04:def 6;
reconsider v = T0 . x, w = T0 . y as Vector of (EMbedding V) ;
thus T0 . (x + y) = (T0 . x) + (T0 . y) by L1, SB01; :: thesis: verum

end;

end;

for x being Vector of V
for i being Element of INT.Ring holds T0 . (i * x) = i * (T0 . x)

proof

let x be Vector of V; :: thesis: for i being Element of INT.Ring holds T0 . (i * x) = i * (T0 . x)
let i be Element of INT.Ring; :: thesis: T0 . (i * x) = i * (T0 . x)
thus T0 . (i * x) = i * (T0 . x) :: thesis: verum

proof

reconsider j = i as Element of F_Rat by NUMBERS:14;
L1: (MorphsZQ V) . (i * x) = j * ((MorphsZQ V) . x) by ZMODUL04:def 6;
reconsider v = T0 . x as Vector of (EMbedding V) ;
thus T0 . (i * x) = i * (T0 . x) by L1, SB01; :: thesis: verum

end;

end;

then ( T0 is additive & T0 is homogeneous ) by B0;
then reconsider T0 = T0 as linear-transformation of V,(EMbedding V) ;
take T0 ; :: thesis: ( T0 is bijective & T0 = MorphsZQ V & ( for v being Vector of V holds T0 . v = Class ((EQRZM V),[v,1]) ) )
SS: T0 is one-to-one by ZMODUL04:def 6;
rng T0 = the carrier of (EMbedding V) by defEmbedding;
then T0 is onto by FUNCT_2:def 3;
hence T0 is bijective by SS; :: thesis: ( T0 = MorphsZQ V & ( for v being Vector of V holds T0 . v = Class ((EQRZM V),[v,1]) ) )
thus T0 = MorphsZQ V ; :: thesis: for v being Vector of V holds T0 . v = Class ((EQRZM V),[v,1])
thus for v being Vector of V holds T0 . v = Class ((EQRZM V),[v,1]) by ZMODUL04:def 6; :: thesis: verum