theorem :: ZMODUL08:26

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