thus for a, b being Element of INT.Ring holds a + b = b + a ; :: according to RLVECT_1:def 5 :: thesis: ( INT.Ring is add-associative & INT.Ring is right_zeroed & INT.Ring is right_complementable & INT.Ring is distributive & INT.Ring is commutative & INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated )
thus for a, b, c being Element of INT.Ring holds (a + b) + c = a + (b + c) ; :: according to RLVECT_1:def 6 :: thesis: ( INT.Ring is right_zeroed & INT.Ring is right_complementable & INT.Ring is distributive & INT.Ring is commutative & INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated )

hereby :: according to RLVECT_1:def 7 :: thesis: ( INT.Ring is right_complementable & INT.Ring is distributive & INT.Ring is commutative & INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated )

let a be Element of INT.Ring ; :: thesis: a + (0. INT.Ring ) = a
A1: a + (0. INT.Ring ) = addreal . a,(0. INT.Ring ) by GR_CY_1:def 2
.= addreal . a,0 by Lm2, FUNCT_7:def 1 ;
reconsider a' = a as Element of REAL by Lm1;
reconsider t = 0 as Element of REAL ;
addreal . a',t = a' + t by BINOP_2:def 9
.= a ;
hence a + (0. INT.Ring ) = a by A1; :: thesis: verum

end;

thus INT.Ring is right_complementable :: thesis: ( INT.Ring is distributive & INT.Ring is commutative & INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated )

proof

let a be Element of INT.Ring ; :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider a' = a as Integer ;
reconsider v = - a' as Element of INT.Ring by INT_1:def 2;
take v ; :: according to ALGSTR_0:def 11 :: thesis: a + v = 0. INT.Ring
thus a + v = 0. INT.Ring by FUNCT_7:def 1; :: thesis: verum

end;

thus for a, b, c being Element of INT.Ring holds
( a * (b + c) = (a * b) + (a * c) & (b + c) * a = (b * a) + (c * a) ) ; :: according to VECTSP_1:def 18 :: thesis: ( INT.Ring is commutative & INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated )
thus for x, y being Element of INT.Ring holds x * y = y * x ; :: according to GROUP_1:def 16 :: thesis: ( INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated )
thus for a, b, c being Element of INT.Ring holds (a * b) * c = a * (b * c) ; :: according to GROUP_1:def 4 :: thesis: ( INT.Ring is domRing-like & not INT.Ring is degenerated )
thus for a, b being Element of INT.Ring holds
( not a * b = 0. INT.Ring or a = 0. INT.Ring or b = 0. INT.Ring ) by Lm3, XCMPLX_1:6; :: according to VECTSP_2:def 5 :: thesis: not INT.Ring is degenerated
thus 0. INT.Ring <> 1. INT.Ring by Lm2, Lm5, FUNCT_7:def 1; :: according to STRUCT_0:def 8 :: thesis: verum