set G = addMagma(# REAL,addreal #);
thus for h, g, f being Element of addMagma(# REAL,addreal #) holds (h + g) + f = h + (g + f) :: according to RLVECT_1:def 3 :: thesis: addMagma(# REAL,addreal #) is addGroup-like

proof

let h, g, f be Element of addMagma(# REAL,addreal #); :: thesis: (h + g) + f = h + (g + f)
reconsider A = h, B = g, C = f as Real ;
A1: g + f = B + C by BINOP_2:def 9;
h + g = A + B by BINOP_2:def 9;
hence (h + g) + f = (A + B) + C by BINOP_2:def 9
.= A + (B + C)
.= h + (g + f) by A1, BINOP_2:def 9 ;
:: thesis: verum

end;

reconsider e = 0 as Element of addMagma(# REAL,addreal #) by XREAL_0:def 1;
take e ; :: according to GROUP_1A:def 2 :: thesis: for h being Element of addMagma(# REAL,addreal #) holds
( h + e = h & e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) )
let h be Element of addMagma(# REAL,addreal #); :: thesis: ( h + e = h & e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) )
reconsider A = h as Real ;
thus h + e = A + 0 by BINOP_2:def 9
.= h ; :: thesis: ( e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) )
thus e + h = 0 + A by BINOP_2:def 9
.= h ; :: thesis: ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e )
reconsider g = - A as Element of addMagma(# REAL,addreal #) by XREAL_0:def 1;
take g ; :: thesis: ( h + g = e & g + h = e )
thus h + g = A + (- A) by BINOP_2:def 9
.= e ; :: thesis: g + h = e
thus g + h = (- A) + A by BINOP_2:def 9
.= e ; :: thesis: verum