thus
for x, y being Element of G_Real holds x + y = y + x
; :: according to RLVECT_1:def 2 :: thesis: ( G_Real is add-associative & G_Real is right_zeroed & G_Real is right_complementable )

thus for x, y, z being Element of G_Real holds (x + y) + z = x + (y + z) ; :: according to RLVECT_1:def 3 :: thesis: ( G_Real is right_zeroed & G_Real is right_complementable )

thus for x being Element of G_Real holds x + (0. G_Real) = x ; :: according to RLVECT_1:def 4 :: thesis: G_Real is right_complementable

let x be Element of G_Real; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable

reconsider x9 = x as Element of REAL ;

reconsider y = - x9 as Element of G_Real by XREAL_0:def 1;

take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. G_Real

thus x + y = 0. G_Real ; :: thesis: verum

thus for x, y, z being Element of G_Real holds (x + y) + z = x + (y + z) ; :: according to RLVECT_1:def 3 :: thesis: ( G_Real is right_zeroed & G_Real is right_complementable )

thus for x being Element of G_Real holds x + (0. G_Real) = x ; :: according to RLVECT_1:def 4 :: thesis: G_Real is right_complementable

let x be Element of G_Real; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable

reconsider x9 = x as Element of REAL ;

reconsider y = - x9 as Element of G_Real by XREAL_0:def 1;

take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. G_Real

thus x + y = 0. G_Real ; :: thesis: verum