thus for a, b being Element of INT.Ring holds a + b = b + a ; :: according to RLVECT_1:def 2 :: 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 3 :: 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 4 :: 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 )

reconsider t = 0 as Element of REAL ;
let a be Element of INT.Ring; :: thesis: a + (0. INT.Ring) = a
reconsider a9 = a as Element of REAL by Lm1;
A1: addreal . (a9,t) = a9 + t by BINOP_2:def 9
.= a ;
a + (0. INT.Ring) = addreal . (a,(0. INT.Ring)) by GR_CY_1:def 1
.= addreal . (a,0) by Lm2, FUNCT_7:def 1 ;
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 a9 = a as Integer ;
reconsider v = - a9 as Element of INT.Ring ;
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 7 :: 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 12 :: 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 3 :: 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 1 :: thesis: not INT.Ring is degenerated
thus 0. INT.Ring <> 1. INT.Ring by Lm2, Lm4, FUNCT_7:def 1; :: according to STRUCT_0:def 8 :: thesis: verum