let AG be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; Z_ModuleStruct(# the carrier of AG, the ZeroF of AG, the addF of AG,(Int-mult-left AG) #) is Z_Module
reconsider ZS = Z_ModuleStruct(# the carrier of AG, the ZeroF of AG, the addF of AG,(Int-mult-left AG) #) as non empty Z_ModuleStruct ;
set ML = the Mult of ZS;
set AD = the addF of ZS;
set CA = the carrier of ZS;
set Z0 = the ZeroF of ZS;
set MLI = Int-mult-left AG;
A1:
for v, w being Element of ZS holds v + w = w + v
proof
let v,
w be
Element of
ZS;
v + w = w + v
reconsider v1 =
v,
w1 =
w as
Element of
AG ;
thus v + w =
v1 + w1
.=
w1 + v1
.=
w + v
;
verum
end;
A2:
for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
A3:
for v being Element of ZS holds v + (0. ZS) = v
A6:
for a, b being Integer
for v being VECTOR of ZS holds (a + b) * v = (a * v) + (b * v)
A7:
for a being Integer
for v, w being VECTOR of ZS holds a * (v + w) = (a * v) + (a * w)
A8:
for a, b being Integer
for v being VECTOR of ZS holds (a * b) * v = a * (b * v)
for v being VECTOR of ZS holds 1 * v = v
hence
Z_ModuleStruct(# the carrier of AG, the ZeroF of AG, the addF of AG,(Int-mult-left AG) #) is Z_Module
by A1, A2, A3, A4, A6, A7, A8, Def2, Def3, Def4, Def5, ALGSTR_0:def 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; verum