let V be torsion-free Z_Module; :: thesis: for vv being Vector of (EMbedding V) ex v being Vector of V st (MorphsZQ V) . v = vv
let vv be Vector of (EMbedding V); :: thesis: ex v being Vector of V st (MorphsZQ V) . v = vv
set Z = EMbedding V;
consider T being linear-transformation of V,(EMbedding V) such that
A1: ( T is bijective & T = MorphsZQ V & ( for v being Element of V holds T . v = Class ((EQRZM V),[v,1]) ) ) by SB03;
vv in the carrier of (EMbedding V) ;
then vv in rng (MorphsZQ V) by A1, FUNCT_2:def 3;
then consider v being object such that
A2: ( v in the carrier of V & vv = (MorphsZQ V) . v ) by FUNCT_2:11;
reconsider v = v as Vector of V by A2;
take v ; :: thesis: (MorphsZQ V) . v = vv
thus (MorphsZQ V) . v = vv by A2; :: thesis: verum