let V be torsion-free Z_Module; :: thesis: 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 ) )
let r be Element of F_Rat; :: thesis: ( ( 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 ) )
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 (r,V);
AS1: ( the carrier of (EMbedding (r,V)) = r * (rng (MorphsZQ V)) & the ZeroF of (EMbedding (r,V)) = zeroCoset V & the addF of (EMbedding (r,V)) = (addCoset V) || (r * (rng (MorphsZQ V))) & the lmult of (EMbedding (r,V)) = (lmultCoset V) | [:INT,(r * (rng (MorphsZQ V))):] ) by defriV;
set Cl = the carrier of (EMbedding (r,V));
set Add = (addCoset V) || the carrier of (EMbedding (r,V));
set Mlt = (lmultCoset V) | [:INT,(r * (rng (MorphsZQ V))):];
X0: the carrier of (EMbedding (r,V)) c= the carrier of (Z_MQ_VectSp V) by AS1;
thus for x being Vector of (EMbedding (r,V)) holds x is Vector of (Z_MQ_VectSp V) by X0; :: thesis: ( 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 ) )
thus 0. (EMbedding (r,V)) = 0. (Z_MQ_VectSp V) by D1, defriV; :: thesis: ( ( 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 ) )
thus 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 :: thesis: 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

proof

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

end;

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

proof

let i be Element of INT.Ring; :: thesis: 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
let j be Element of F_Rat; :: thesis: 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
let x be Vector of (EMbedding (r,V)); :: thesis: for v being Vector of (Z_MQ_VectSp V) st i = j & x = v holds
i * x = j * v
let v be Vector of (Z_MQ_VectSp V); :: thesis: ( i = j & x = v implies i * x = j * v )
assume L0: ( i = j & x = v ) ; :: thesis: i * x = j * v
thus i * x = (lmultCoset V) . [i,x] by AS1, FUNCT_1:49
.= j * v by D1, L0 ; :: thesis: verum

end;