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 ) ;
set Cl = rng (MorphsZQ V);
set Add = (addCoset V) || (rng (MorphsZQ V));
set Mlt = (lmultCoset V) | [: the carrier of INT.Ring,(rng (MorphsZQ V)):];
X0: 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) || (rng (MorphsZQ V))) = [:(rng (MorphsZQ V)),(rng (MorphsZQ V)):] by RELAT_1:62;
for x being object st x in [:(rng (MorphsZQ V)),(rng (MorphsZQ V)):] holds
((addCoset V) || (rng (MorphsZQ V))) . x in rng (MorphsZQ V)

proof

let x be object ; :: thesis:
assume X40: x in [:(rng (MorphsZQ V)),(rng (MorphsZQ V)):] ; :: thesis:
then consider v, w being object such that
X41: ( v in rng (MorphsZQ V) & w in rng (MorphsZQ V) & x = [v,w] ) by ZFMISC_1:def 2;
consider a being object such that
X43: ( a in the carrier of V & v = (MorphsZQ V) . a ) by X41, FUNCT_2:11;
reconsider a = a as Vector of V by X43;
X44: v = Class ((EQRZM V),[a,1]) by ZMODUL04:def 6, X43;
consider b being object such that
X45: ( b in the carrier of V & w = (MorphsZQ V) . b ) by X41, FUNCT_2:11;
reconsider b = b as Vector of V by X45;
X46: w = Class ((EQRZM V),[b,1]) by ZMODUL04:def 6, X45;
((addCoset V) || (rng (MorphsZQ V))) . x = (addCoset V) . (v,w) by X40, X41, FUNCT_1:49
.= Class ((EQRZM V),[(((1. INT.Ring) * a) + ((1. INT.Ring) * b)),((1. INT.Ring) * (1. INT.Ring))]) by D1, X41, X44, X46, ZMODUL04:def 2
.= Class ((EQRZM V),[(a + ((1. INT.Ring) * b)),1]) by VECTSP_1:def 17
.= Class ((EQRZM V),[(a + b),1]) by VECTSP_1:def 17
.= (MorphsZQ V) . (a + b) by ZMODUL04:def 6 ;
hence ((addCoset V) || (rng (MorphsZQ V))) . x in rng (MorphsZQ V) by FUNCT_2:4; :: thesis:

end;

then reconsider Add = (addCoset V) || (rng (MorphsZQ V)) as BinOp of (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) | [: the carrier of INT.Ring,(rng (MorphsZQ V)):]) = [: the carrier of INT.Ring,(rng (MorphsZQ V)):] by RELAT_1:62, NUMBERS:14, ZFMISC_1:96;
for x being object st x in [: the carrier of INT.Ring,(rng (MorphsZQ V)):] holds
((lmultCoset V) | [: the carrier of INT.Ring,(rng (MorphsZQ V)):]) . x in rng (MorphsZQ V)

proof

let x be object ; :: thesis:
assume X40: x in [: the carrier of INT.Ring,(rng (MorphsZQ V)):] ; :: thesis:
then consider i, w being object such that
X41: ( i in INT & w in rng (MorphsZQ V) & x = [i,w] ) by ZFMISC_1:def 2;
consider b being object such that
X45: ( b in the carrier of V & w = (MorphsZQ V) . b ) by X41, FUNCT_2:11;
reconsider b = b as Vector of V by X45;
reconsider i = i as Element of INT.Ring by X41;
reconsider j = i as Element of F_Rat by NUMBERS:14;
X47: ( j = i / 1 & 1 <> 0 ) ;
X46: w = Class ((EQRZM V),[b,1]) by ZMODUL04:def 6, X45;
((lmultCoset V) | [: the carrier of INT.Ring,(rng (MorphsZQ V)):]) . x = (lmultCoset V) . (j,w) by X40, X41, FUNCT_1:49
.= Class ((EQRZM V),[(i * b),(1 * 1)]) by D1, X41, X46, X47, ZMODUL04:def 4
.= (MorphsZQ V) . (i * b) by ZMODUL04:def 6 ;
hence ((lmultCoset V) | [: the carrier of INT.Ring,(rng (MorphsZQ V)):]) . x in rng (MorphsZQ V) by FUNCT_2:4; :: thesis:

end;

then reconsider Mlt = (lmultCoset V) | [: the carrier of INT.Ring,(rng (MorphsZQ V)):] as Function of [: the carrier of INT.Ring,(rng (MorphsZQ V)):],(rng (MorphsZQ V)) by Y3, FUNCT_2:3;
X1: (MorphsZQ V) . (0. V) = 0. (Z_MQ_VectSp V) by ZMODUL04:def 6
.= zeroCoset V by D1 ;
reconsider z = zeroCoset V as Element of rng (MorphsZQ V) by X1, FUNCT_2:4;
set ZS = ModuleStr(# (rng (MorphsZQ V)),Add,z,Mlt #);
reconsider ZS = ModuleStr(# (rng (MorphsZQ V)),Add,z,Mlt #) as non empty ModuleStr over INT.Ring ;
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:
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 FUNCT_1:49
.= v + w by D1, L0 ; :: thesis:

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:
let j be Element of F_Rat; :: thesis:
let x be Vector of ZS; :: 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 FUNCT_1:49
.= j * v by D1, L0 ; :: thesis:

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:
let v, w be Element of ZS; :: thesis:
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:

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:
let v be Element of ZS; :: thesis:
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:

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:
let v be Element of ZS; :: thesis:
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:

end;

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

proof

let v be Element of ZS; :: thesis:
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:

end;

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

proof

let v be Element of ZS; :: thesis:
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:

end;

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

proof

let v, w be Element of ZS; :: thesis:
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:

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

end;

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

proof

let v be Element of ZS; :: thesis:
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:

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:

end;

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