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;
AX: ( Z_MQ_VectSp V is scalar-distributive & Z_MQ_VectSp V is vector-distributive & Z_MQ_VectSp V is scalar-associative & Z_MQ_VectSp V is scalar-unital & Z_MQ_VectSp V is add-associative & Z_MQ_VectSp V is right_zeroed & Z_MQ_VectSp V is right_complementable & Z_MQ_VectSp V is Abelian & not Z_MQ_VectSp V is empty ) ;
BX: rng (MorphsZQ V) = the carrier of (EMbedding V) by defEmbedding;
set Cl = r * (rng (MorphsZQ V));
set Add = (addCoset V) || (r * (rng (MorphsZQ V)));
set Mlt = (lmultCoset V) | [:INT,(r * (rng (MorphsZQ V))):];
X0: r * (rng (MorphsZQ V)) c= the carrier of (Z_MQ_VectSp V) ;
dom (addCoset V) = [: the carrier of (Z_MQ_VectSp V), the carrier of (Z_MQ_VectSp V):] by D1, FUNCT_2:def 1;
then X3: dom ((addCoset V) || (r * (rng (MorphsZQ V)))) = [:(r * (rng (MorphsZQ V))),(r * (rng (MorphsZQ V))):] by RELAT_1:62;
for x being object st x in [:(r * (rng (MorphsZQ V))),(r * (rng (MorphsZQ V))):] holds
((addCoset V) || (r * (rng (MorphsZQ V)))) . x in r * (rng (MorphsZQ V))

proof

let x be object ; :: thesis: ( x in [:(r * (rng (MorphsZQ V))),(r * (rng (MorphsZQ V))):] implies ((addCoset V) || (r * (rng (MorphsZQ V)))) . x in r * (rng (MorphsZQ V)) )
assume X40: x in [:(r * (rng (MorphsZQ V))),(r * (rng (MorphsZQ V))):] ; :: thesis: ((addCoset V) || (r * (rng (MorphsZQ V)))) . x in r * (rng (MorphsZQ V))
then consider v0, w0 being object such that
X41: ( v0 in r * (rng (MorphsZQ V)) & w0 in r * (rng (MorphsZQ V)) & x = [v0,w0] ) by ZFMISC_1:def 2;
consider v being Vector of (Z_MQ_VectSp V) such that
X410: ( v0 = r * v & v in rng (MorphsZQ V) ) by X41;
consider w being Vector of (Z_MQ_VectSp V) such that
X411: ( w0 = r * w & w in rng (MorphsZQ V) ) by X41;
( v in EMbedding V & w in EMbedding V ) by X410, X411, defEmbedding;
then X42: v + w in EMbedding V by SB02;
((addCoset V) || (r * (rng (MorphsZQ V)))) . x = (r * v) + (r * w) by X40, X41, X410, X411, D1, FUNCT_1:49
.= r * (v + w) by VECTSP_1:def 14 ;
hence ((addCoset V) || (r * (rng (MorphsZQ V)))) . x in r * (rng (MorphsZQ V)) by BX, X42; :: thesis: verum

end;

then reconsider Add = (addCoset V) || (r * (rng (MorphsZQ V))) as BinOp of (r * (rng (MorphsZQ V))) by X3, FUNCT_2:3;
dom (lmultCoset V) = [: the carrier of F_Rat, the carrier of (Z_MQ_VectSp V):] by FUNCT_2:def 1, D1;
then Y3: dom ((lmultCoset V) | [:INT,(r * (rng (MorphsZQ V))):]) = [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] by RELAT_1:62, NUMBERS:14, ZFMISC_1:96;
for x being object st x in [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] holds
((lmultCoset V) | [:INT,(r * (rng (MorphsZQ V))):]) . x in r * (rng (MorphsZQ V))

proof

let x be object ; :: thesis: ( x in [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] implies ((lmultCoset V) | [:INT,(r * (rng (MorphsZQ V))):]) . x in r * (rng (MorphsZQ V)) )
assume X40: x in [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] ; :: thesis: ((lmultCoset V) | [:INT,(r * (rng (MorphsZQ V))):]) . x in r * (rng (MorphsZQ V))
then consider i, w0 being object such that
X41: ( i in INT & w0 in r * (rng (MorphsZQ V)) & x = [i,w0] ) by ZFMISC_1:def 2;
reconsider i1 = i as Integer by X41;
reconsider i2 = i as Element of F_Rat by X41, NUMBERS:14;
consider w being Vector of (Z_MQ_VectSp V) such that
X411: ( w0 = r * w & w in rng (MorphsZQ V) ) by X41;
w in EMbedding V by X411, defEmbedding;
then X42: i2 * w in EMbedding V by SB02, X41;
((lmultCoset V) | [:INT,(r * (rng (MorphsZQ V))):]) . x = i2 * (r * w) by D1, X40, X411, X41, FUNCT_1:49
.= (i2 * r) * w by VECTSP_1:def 16
.= r * (i2 * w) by VECTSP_1:def 16 ;
hence ((lmultCoset V) | [:INT,(r * (rng (MorphsZQ V))):]) . x in r * (rng (MorphsZQ V)) by BX, X42; :: thesis: verum

end;

then reconsider Mlt = (lmultCoset V) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] as Function of [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):],(r * (rng (MorphsZQ V))) by Y3, FUNCT_2:3;
X1: r * (0. (Z_MQ_VectSp V)) = 0. (Z_MQ_VectSp V) by VECTSP_1:15;
0. (Z_MQ_VectSp V) = 0. (EMbedding V) by D1, defEmbedding;
then X2: 0. (Z_MQ_VectSp V) in r * (rng (MorphsZQ V)) by BX, X1;
reconsider z = zeroCoset V as Element of r * (rng (MorphsZQ V)) by D1, X2;
set ZS = ModuleStr(# (r * (rng (MorphsZQ V))),Add,z,Mlt #);
reconsider ZS = ModuleStr(# (r * (rng (MorphsZQ V))),Add,z,Mlt #) as non empty ModuleStr over INT.Ring by X2;
LM2: for x, y being Vector of ZS
for v, w being Vector of (Z_MQ_VectSp V) st x = v & y = w holds
x + y = v + w

proof

let x, y be Vector of ZS; :: 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 FUNCT_1:49
.= v + w by D1, L0 ; :: thesis: verum

end;

LM3: for i being Element of INT.Ring
for j being Element of F_Rat
for x being Vector of ZS
for v being Vector of (Z_MQ_VectSp V) st i = j & x = v holds
i * x = j * v

proof

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

end;

ZS is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over INT.Ring

proof

P1: for x being Element of INT.Ring
for v, w being Element of ZS holds x * (v + w) = (x * v) + (x * w)

proof

let x be Element of INT.Ring; :: thesis: for v, w being Element of ZS holds x * (v + w) = (x * v) + (x * w)
let v, w be Element of ZS; :: thesis: x * (v + w) = (x * v) + (x * w)
reconsider y = x as Element of F_Rat by NUMBERS:14;
reconsider s = v, t = w as Vector of (Z_MQ_VectSp V) by X0;
P1: v + w = s + t by LM2;
P2: ( x * v = y * s & x * w = y * t ) by LM3;
thus x * (v + w) = y * (s + t) by P1, LM3
.= (y * s) + (y * t) by AX
.= (x * v) + (x * w) by LM2, P2 ; :: thesis: verum

end;

P2: for x, y being Element of INT.Ring
for v being Element of ZS holds (x + y) * v = (x * v) + (y * v)

proof

let x, y be Element of INT.Ring; :: thesis: for v being Element of ZS holds (x + y) * v = (x * v) + (y * v)
let v be Element of ZS; :: thesis: (x + y) * v = (x * v) + (y * v)
reconsider p = x, q = y as Element of F_Rat by NUMBERS:14;
reconsider p1 = p, q1 = q as Rational ;
reconsider s = v as Vector of (Z_MQ_VectSp V) by X0;
P1: x * v = p * s by LM3;
P2: y * v = q * s by LM3;
thus (x + y) * v = (p + q) * s by LM3
.= (p * s) + (q * s) by AX
.= (x * v) + (y * v) by P1, P2, LM2 ; :: thesis: verum

end;

P3: for x, y being Element of INT.Ring
for v being Element of ZS holds (x * y) * v = x * (y * v)

proof

let x, y be Element of INT.Ring; :: thesis: for v being Element of ZS holds (x * y) * v = x * (y * v)
let v be Element of ZS; :: thesis: (x * y) * v = x * (y * v)
reconsider p = x, q = y as Element of F_Rat by NUMBERS:14;
reconsider p1 = p, q1 = q as Rational ;
reconsider s = v as Vector of (Z_MQ_VectSp V) by X0;
P1: y * v = q * s by LM3;
thus (x * y) * v = (p * q) * s by LM3
.= p * (q * s) by AX
.= x * (y * v) by P1, LM3 ; :: thesis: verum

end;

P4: for v being Element of ZS holds (1. INT.Ring) * v = v

proof

let v be Element of ZS; :: thesis: (1. INT.Ring) * v = v
reconsider s = v as Vector of (Z_MQ_VectSp V) by X0;
thus (1. INT.Ring) * v = (1. F_Rat) * s by LM3
.= v by AX ; :: thesis: verum

end;

P5: for v being Element of ZS holds v is right_complementable

proof

let v be Element of ZS; :: thesis: v is right_complementable
reconsider s = v as Vector of (Z_MQ_VectSp V) by X0;
reconsider i1 = 1. F_Rat as Rational ;
P5: - s = (- (1. F_Rat)) * s by VECTSP_1:14;
P1: (- (1. INT.Ring)) * v = (- (1. F_Rat)) * s by LM3;
v + ((- (1. INT.Ring)) * v) = s - s by P1, P5, LM2
.= 0. (Z_MQ_VectSp V) by RLVECT_1:15
.= 0. ZS by D1 ;
hence v is right_complementable ; :: thesis: verum

end;

P6: for v, w being Element of ZS holds v + w = w + v

proof

let v, w be Element of ZS; :: thesis: v + w = w + v
reconsider s = v, t = w as Vector of (Z_MQ_VectSp V) by X0;
thus v + w = s + t by LM2
.= w + v by LM2 ; :: thesis: verum

end;

P7: for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)

proof

let u, v, w be Element of ZS; :: thesis: (u + v) + w = u + (v + w)
reconsider z = u, s = v, t = w as Vector of (Z_MQ_VectSp V) by X0;
P1: u + v = z + s by LM2;
P2: v + w = s + t by LM2;
thus (u + v) + w = (z + s) + t by P1, LM2
.= z + (s + t) by RLVECT_1:def 3
.= u + (v + w) by LM2, P2 ; :: thesis: verum

end;

for v being Element of ZS holds v + (0. ZS) = v

proof

let v be Element of ZS; :: thesis: v + (0. ZS) = v
reconsider s = v as Vector of (Z_MQ_VectSp V) by X0;
thus v + (0. ZS) = s + (0. (Z_MQ_VectSp V)) by LM2, D1
.= v ; :: thesis: verum

end;

hence ZS is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over INT.Ring by P1, P2, P3, P4, P5, P6, P7, ALGSTR_0:def 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17; :: thesis: verum

end;

then reconsider ZS = ZS as strict Z_Module ;
take ZS ; :: thesis: ( the carrier of ZS = r * (rng (MorphsZQ V)) & the ZeroF of ZS = zeroCoset V & the addF of ZS = (addCoset V) || (r * (rng (MorphsZQ V))) & the lmult of ZS = (lmultCoset V) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] )
thus ( the carrier of ZS = r * (rng (MorphsZQ V)) & the ZeroF of ZS = zeroCoset V & the addF of ZS = (addCoset V) || (r * (rng (MorphsZQ V))) & the lmult of ZS = (lmultCoset V) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] ) ; :: thesis: verum