reconsider ZS = ModuleStr(# G_INT_SET,g_int_add,(In (0,G_INT_SET)),Sc_Mult #) as non empty ModuleStr over INT.Ring ;
set AG = G_INT_SET ;
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 = Sc_Mult ;
A1:
for v, w being Element of ZS holds v + w = w + v
A2:
for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
A5:
for v being Element of ZS holds v + (0. ZS) = v
A6:
for v being Vector of ZS holds v is right_complementable
A8:
for a, b being Element of INT.Ring
for v being Vector of ZS holds (a + b) * v = (a * v) + (b * v)
A10:
for a being Element of INT.Ring
for v, w being Vector of ZS holds a * (v + w) = (a * v) + (a * w)
A13:
for a, b being Element of INT.Ring
for v being Vector of ZS holds (a * b) * v = a * (b * v)
for v being Vector of ZS holds (1. INT.Ring) * v = v
hence
Gauss_INT_Module is Z_Module
by A1, A2, A5, A6, A8, A10, A13, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, ALGSTR_0:def 16; verum