reconsider ZS = doubleLoopStr(# G_INT_SET,g_int_add,g_int_mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) as non empty doubleLoopStr ;
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 Element of ZS holds v is right_complementable

proof

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

end;

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

proof

let a, b, v be Element of ZS; :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider a1 = a, b1 = b, v1 = v as G_INTEG by Th2;
reconsider ab = a + b as G_INTEG by Th2;
A9: ( a1 * v1 = a * v & b1 * v1 = b * v ) by Th6;
thus (a + b) * v = ab * v1 by Th6
.= (a1 + b1) * v1 by Th4
.= (a1 * v1) + (b1 * v1)
.= (a * v) + (b * v) by A9, Th4 ; :: thesis: verum

end;

A10: for a, v, w being Element of ZS holds
( a * (v + w) = (a * v) + (a * w) & (v + w) * a = (v * a) + (w * a) )

proof

let a, v, w be Element of ZS; :: thesis: ( a * (v + w) = (a * v) + (a * w) & (v + w) * a = (v * a) + (w * a) )
reconsider a1 = a, v1 = v, w1 = w as G_INTEG by Th2;
reconsider vw = v + w as G_INTEG by Th2;
A11: ( a1 * v1 = a * v & a1 * w1 = a * w ) by Th6;
thus a * (v + w) = a1 * vw by Th6
.= a1 * (v1 + w1) by Th4
.= (a1 * v1) + (a1 * w1)
.= (a * v) + (a * w) by A11, Th4 ; :: thesis: (v + w) * a = (v * a) + (w * a)
thus (v + w) * a = (v * a) + (w * a) by A8; :: thesis: verum

end;

A12: for a, b, v being Element of ZS holds (a * b) * v = a * (b * v)

proof

let a, b, v be Element of ZS; :: thesis: (a * b) * v = a * (b * v)
reconsider a1 = a, b1 = b, v1 = v as G_INTEG by Th2;
reconsider ab = a * b, bv = b * v as G_INTEG by Th2;
thus (a * b) * v = ab * v1 by Th6
.= (a1 * b1) * v1 by Th6
.= a1 * (b1 * v1)
.= a1 * bv by Th6
.= a * (b * v) by Th6 ; :: thesis: verum

end;

for v being Element of ZS holds
( v * (1. ZS) = v & (1. ZS) * v = v )

proof

let v be Element of ZS; :: thesis: ( v * (1. ZS) = v & (1. ZS) * v = v )
reconsider v1 = v as G_INTEG by Th2;
thus v * (1. ZS) = v1 * 1 by Th6
.= v ; :: thesis: (1. ZS) * v = v
thus (1. ZS) * v = 1 * v1 by Th6
.= v ; :: thesis: verum

end;

hence Gauss_INT_Ring is Ring by A1, A2, A5, A6, A10, A12, VECTSP_1:def 6, VECTSP_1:def 7, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, ALGSTR_0:def 16; :: thesis: verum