let V be free finite-rank Z_Module; :: thesis: rank (EMbedding V) = rank V
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;
thus rank (EMbedding V) = rank V by A1, ZMODUL06:51; :: thesis: verum