thus for x, y being Element of holds x + y = y + x ; :: according to RLVECT_1:def 5 :: thesis: ( G_Real is add-associative & G_Real is right_zeroed & G_Real is right_complementable )
thus for x, y, z being Element of holds (x + y) + z = x + (y + z) ; :: according to RLVECT_1:def 6 :: thesis: ( G_Real is right_zeroed & G_Real is right_complementable )
thus for x being Element of holds x + (0. G_Real ) = x ; :: according to RLVECT_1:def 7 :: thesis: G_Real is right_complementable
let x be Element of ; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x' = x as Element of REAL ;
reconsider y = - x' as Element of ;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. G_Real
thus x + y = 0. G_Real ; :: thesis: verum