let V be torsion-free Z_Module; for v being Vector of V holds Class ((EQRZM V),[v,1]) in EMbedding V
let v be Vector of V; 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; verum