reconsider G = addMagma(# REAL,addreal #) as addGroup by Th3;
G is Abelian

proof

let h, g be Element of G; :: according to RLVECT_1:def 2 :: thesis: h + g = g + h
reconsider A = h, B = g as Real ;
thus h + g = B + A by BINOP_2:def 9
.= g + h by BINOP_2:def 9 ; :: thesis: verum

end;

hence addMagma(# REAL,addreal #) is Abelian addGroup ; :: thesis: verum