let V be torsion-free Z_Module; :: thesis: for v being Vector of V holds Class ((EQRZM V),[v,1]) in EMbedding V
let v be Vector of V; :: thesis: Class ((EQRZM V),[v,1]) in EMbedding V
(MorphsZQ V) . v = Class ((EQRZM V),[v,1]) by ZMODUL04:def 6;
then Class ((EQRZM V),[v,1]) in rng (MorphsZQ V) by FUNCT_2:4;
hence Class ((EQRZM V),[v,1]) in EMbedding V by defEmbedding; :: thesis: verum