theorem SB02: :: ZMODUL08:20

for V being torsion-free Z_Module holds
( ( for v, w being Vector of (Z_MQ_VectSp V) st v in EMbedding V & w in EMbedding V holds
v + w in EMbedding V ) & ( for j being Element of F_Rat
for v being Vector of (Z_MQ_VectSp V) st j in INT & v in EMbedding V holds
j * v in EMbedding V ) )