let V be torsion-free Z_Module; :: thesis:
set EZV = Z_MQ_VectSp V;
D1: Z_MQ_VectSp V = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) by ZMODUL04:def 5;
set ZS = EMbedding V;
AS1: ( the carrier of (EMbedding V) = rng (MorphsZQ V) & the ZeroF of (EMbedding V) = zeroCoset V & the addF of (EMbedding V) = (addCoset V) || (rng (MorphsZQ V)) & the lmult of (EMbedding V) = (lmultCoset V) | [: the carrier of INT.Ring,(rng (MorphsZQ V)):] ) by defEmbedding;
set Cl = the carrier of (EMbedding V);
set Add = (addCoset V) || the carrier of (EMbedding V);
set Mlt = (lmultCoset V) | [: the carrier of INT.Ring,(rng (MorphsZQ V)):];
the carrier of (EMbedding V) c= the carrier of (Z_MQ_VectSp V) by AS1;
hence for x being Vector of (EMbedding V) holds x is Vector of (Z_MQ_VectSp V) ; :: thesis:
thus 0. (EMbedding V) = 0. (Z_MQ_VectSp V) by D1, defEmbedding; :: thesis:
thus 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 :: thesis:

let x, y be Vector of (EMbedding V); :: thesis:
let v, w be Vector of (Z_MQ_VectSp V); :: thesis:
assume L0: ( x = v & y = w ) ; :: thesis:
thus x + y = (addCoset V) . [x,y] by AS1, FUNCT_1:49
.= v + w by D1, L0 ; :: thesis:

end;

thus 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 :: thesis:

let i be Element of INT.Ring; :: thesis:
let j be Element of F_Rat; :: thesis:
let x be Vector of (EMbedding V); :: thesis:
let v be Vector of (Z_MQ_VectSp V); :: thesis:
assume L0: ( i = j & x = v ) ; :: thesis:
thus i * x = (lmultCoset V) . [i,x] by AS1, FUNCT_1:49
.= j * v by D1, L0 ; :: thesis:

end;