for V being torsion-free Z_Module
for r being Element of F_Rat holds
( ( for x being Vector of (EMbedding (r,V)) holds x is Vector of (Z_MQ_VectSp V) ) & 0. (EMbedding (r,V)) = 0. (Z_MQ_VectSp V) & ( for x, y being Vector of (EMbedding (r,V))
for v, w being Vector of (Z_MQ_VectSp V) st x = v & y = w holds
x + y = v + w ) & ( for i being Element of INT.Ring
for j being Element of F_Rat
for x being Vector of (EMbedding (r,V))
for v being Vector of (Z_MQ_VectSp V) st i = j & x = v holds
i * x = j * v ) )