consider T being linear-transformation of (EMbedding V),(EMbedding (r,V)) such that
A1: ( ( for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds
T . v = r * v ) & T is bijective ) by rSB03A;
thus EMbedding (r,V) is free by A1, ZMODUL06:48; :: thesis: verum