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

proof

let v, w be Element of ZS; :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as G_INTEG by Th2;
thus v + w = w1 + v1 by Th4
.= w + v by Th4 ; :: thesis: verum

end;

A2: 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: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as G_INTEG by Th2;
A3: u + v = u1 + v1 by Th4;
A4: v + w = v1 + w1 by Th4;
thus (u + v) + w = (u1 + v1) + w1 by Th4, A3
.= u1 + (v1 + w1)
.= u + (v + w) by Th4, A4 ; :: thesis: verum

end;

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

proof

let v be Element of ZS; :: thesis: v + (0. ZS) = v
reconsider v1 = v as G_INTEG by Th2;
thus v + (0. ZS) = v1 + 0 by Th4
.= v ; :: thesis: verum

end;

A6: for v being Vector of ZS holds v is right_complementable

proof

let v be Vector of ZS; :: thesis: v is right_complementable
take (- (1. INT.Ring)) * v ; :: according to ALGSTR_0:def 11 :: thesis: v + ((- (1. INT.Ring)) * v) = 0. ZS
reconsider v1 = v as G_INTEG by Th2;
A7: (- (1. INT.Ring)) * v = (- 1) * v1 by LmX, Th5
.= - v1 ;
thus v + ((- (1. INT.Ring)) * v) = v1 + (- v1) by A7, Th4
.= 0. ZS ; :: thesis: verum

end;

A8: for a, b being Element of INT.Ring
for v being Vector of ZS holds (a + b) * v = (a * v) + (b * v)

proof

let a, b be Element of INT.Ring; :: thesis: for v being Vector of ZS holds (a + b) * v = (a * v) + (b * v)
let v be Vector of ZS; :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v1 = v as G_INTEG by Th2;
A9: ( a * v1 = a * v & b * v1 = b * v ) by Th5;
thus (a + b) * v = (a + b) * v1 by Th5
.= (a * v1) + (b * v1)
.= (a * v) + (b * v) by A9, Th4 ; :: thesis: verum

end;

A10: for a being Element of INT.Ring
for v, w being Vector of ZS holds a * (v + w) = (a * v) + (a * w)

proof

let a be Element of INT.Ring; :: thesis: for v, w being Vector of ZS holds a * (v + w) = (a * v) + (a * w)
let v, w be Vector of ZS; :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v1 = v, w1 = w as G_INTEG by Th2;
A11: v + w = v1 + w1 by Th4;
A12: ( a * v1 = a * v & a * w1 = a * w ) by Th5;
thus a * (v + w) = a * (v1 + w1) by A11, Th5
.= (a * v1) + (a * w1)
.= (a * v) + (a * w) by A12, Th4 ; :: thesis: verum

end;

A13: for a, b being Element of INT.Ring
for v being Vector of ZS holds (a * b) * v = a * (b * v)

proof

let a, b be Element of INT.Ring; :: thesis: for v being Vector of ZS holds (a * b) * v = a * (b * v)
let v be Vector of ZS; :: thesis: (a * b) * v = a * (b * v)
reconsider v1 = v as G_INTEG by Th2;
A14: b * v1 = b * v by Th5;
thus (a * b) * v = (a * b) * v1 by Th5
.= a * (b * v1)
.= a * (b * v) by A14, Th5 ; :: thesis: verum

end;

for v being Vector of ZS holds (1. INT.Ring) * v = v

proof

let v be Vector of ZS; :: thesis: (1. INT.Ring) * v = v
set i = 1. INT.Ring;
reconsider v1 = v as G_INTEG by Th2;
thus (1. INT.Ring) * v = 1 * v1 by Th5, INT_3:def 3
.= v ; :: thesis: verum

end;

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; :: thesis: verum