let AG be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ModuleStr(# the carrier of AG, the addF of AG, the ZeroF of AG,(Int-mult-left AG) #) is Z_Module
reconsider ZS = ModuleStr(# the carrier of AG, the addF of AG, the ZeroF of AG,(Int-mult-left AG) #) as non empty ModuleStr over INT.Ring ;
set ML = the lmult 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 Element of INT.Ring
for v being Vector of ZS holds (a + b) * v = (a * v) + (b * v)
A7:
for a being Element of INT.Ring
for v, w being Vector of ZS holds a * (v + w) = (a * v) + (a * w)
A8:
for a, b being Element of INT.Ring
for v being Vector of ZS holds (a * b) * v = a * (b * v)
by Th163;
for v being Vector of ZS holds (1. INT.Ring) * v = v
by Th155;
hence
ModuleStr(# the carrier of AG, the addF of AG, the ZeroF of AG,(Int-mult-left AG) #) is Z_Module
by A1, A2, A3, A4, A6, A7, A8, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17, ALGSTR_0:def 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; verum