consider T being linear-transformation of V,(EMbedding V) such that
A1: ( T is bijective & T = MorphsZQ V & ( for v being Vector of V holds T . v = Class ((EQRZM V),[v,1]) ) ) by SB03;
reconsider Z = EMbedding V as free Z_Module by A1, ZMODUL06:48;
Z is finite-rank by A1, ZMODUL06:50;
hence EMbedding V is finitely-generated ; :: thesis: verum