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 )
thus for a being Element of INT.Ring holds a + (0. INT.Ring) = a ; :: 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 )
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 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 ; :: 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 XCMPLX_1:6; :: according to VECTSP_2:def 1 :: thesis: not INT.Ring is degenerated
thus 0. INT.Ring <> 1. INT.Ring ; :: according to STRUCT_0:def 8 :: thesis: verum