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 EMbedding V is free by A1, ZMODUL06:48; :: thesis: verum