theorem SB01: :: ZMODUL08:19

for V being torsion-free Z_Module holds
( ( for x being Vector of (EMbedding V) holds x is Vector of (Z_MQ_VectSp V) ) & 0. (EMbedding V) = 0. (Z_MQ_VectSp V) & ( for x, y being Vector of (EMbedding 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 V)
for v being Vector of (Z_MQ_VectSp V) st i = j & x = v holds
i * x = j * v ) )