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