let V be torsion-free Z_Module; :: thesis: ( ( 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 ) )
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: ( 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 ) )
thus 0. (EMbedding V) = 0. (Z_MQ_VectSp V) by D1, defEmbedding; :: thesis: ( ( 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 ) )
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: 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

proof

let x, y be Vector of (EMbedding 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 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 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 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 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;