set X0 = the carrier of X;
set Z0 = the ZeroF of X;
set ADD = the addF of X;
set VMLT = Mult_INT* X;
set XQ = Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #);
A1: for vd, wd being Element of X
for v, w being Element of Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) st v = vd & w = wd holds
v + w = vd + wd ;
( Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is Abelian & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is add-associative & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is right_zeroed & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is right_complementable & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-distributive & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is vector-distributive & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-associative & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-unital )

proof

hereby :: according to RLVECT_1:def 2 :: thesis: ( Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is add-associative & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is right_zeroed & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is right_complementable & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-distributive & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is vector-distributive & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-associative & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-unital )

let v, w be VECTOR of Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #); :: thesis: v + w = w + v
reconsider vd = v, wd = w as Element of X ;
thus v + w = wd + vd by A1
.= w + v ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is right_zeroed & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is right_complementable & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-distributive & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is vector-distributive & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-associative & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-unital )

let u, v, w be VECTOR of Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #); :: thesis: (u + v) + w = u + (v + w)
reconsider ud = u, vd = v, wd = w as Element of X ;
thus (u + v) + w = (ud + vd) + wd
.= ud + (vd + wd) by RLVECT_1:def 3
.= u + (v + w) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 4 :: thesis: ( Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is right_complementable & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-distributive & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is vector-distributive & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-associative & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-unital )

let v be VECTOR of Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #); :: thesis: v + (0. Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #)) = v
reconsider vd = v as Element of X ;
thus v + (0. Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #)) = vd + (0. X)
.= v by RLVECT_1:4 ; :: thesis: verum

end;

thus Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is right_complementable :: thesis: ( Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-distributive & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is vector-distributive & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-associative & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-unital )

proof

let v be VECTOR of Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider vd = v as Element of X ;
consider wd being Element of X such that
A2: vd + wd = 0. X by ALGSTR_0:def 11;
reconsider w = wd as VECTOR of Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #)
thus v + w = 0. Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) by A2; :: thesis: verum

end;

hereby :: according to ZMODUL01:def 3 :: thesis: ( Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is vector-distributive & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-associative & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-unital )

let a, b be Integer; :: thesis: for v being VECTOR of Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider vd = v as Element of X ;
reconsider ad = a as Scalar of INT.Ring by INT_1:def 2;
reconsider bd = b as Scalar of INT.Ring by INT_1:def 2;
thus (a + b) * v = (ad + bd) * vd
.= (ad * vd) + (bd * vd) by VECTSP_1:def 15
.= (a * v) + (b * v) ; :: thesis: verum

end;

hereby :: according to ZMODUL01:def 2 :: thesis: ( Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-associative & Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-unital )

let a be Integer; :: thesis: for v, w being VECTOR of Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #); :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider ad = a as Element of INT.Ring by INT_1:def 2;
reconsider vd = v, wd = w as Element of X ;
thus a * (v + w) = ad * (vd + wd)
.= (ad * vd) + (ad * wd) by VECTSP_1:def 14
.= (a * v) + (a * w) ; :: thesis: verum

end;

hereby :: according to ZMODUL01:def 4 :: thesis: Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) is scalar-unital

let a, b be Integer; :: thesis: for v being VECTOR of Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #) holds (a * b) * v = a * (b * v)
let v be VECTOR of Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #); :: thesis: (a * b) * v = a * (b * v)
reconsider vd = v as Element of X ;
reconsider ad = a as Scalar of INT.Ring by INT_1:def 2;
reconsider bd = b as Scalar of INT.Ring by INT_1:def 2;
thus (a * b) * v = (ad * bd) * vd
.= ad * (bd * vd) by VECTSP_1:def 16
.= a * (b * v) ; :: thesis: verum

end;

let v be VECTOR of Z_ModuleStruct(# the carrier of X, the ZeroF of X, the addF of X,(Mult_INT* X) #); :: according to ZMODUL01:def 5 :: thesis: 1 * v = v
reconsider vd = v as Element of X ;
thus 1 * v = (1. INT.Ring) * vd
.= v by VECTSP_1:def 17 ; :: thesis: verum

end;

hence ( modetrans X is Abelian & modetrans X is add-associative & modetrans X is right_zeroed & modetrans X is right_complementable & modetrans X is scalar-distributive & modetrans X is vector-distributive & modetrans X is scalar-associative & modetrans X is scalar-unital ) ; :: thesis: verum