reconsider G0 = addMagma(# REAL,addreal #) as addGroup by Th3;
take G0 ; :: thesis: ( G0 is strict & G0 is Abelian )
thus G0 is strict ; :: thesis: G0 is Abelian
let a, g be Element of G0; :: according to RLVECT_1:def 2 :: thesis: a + g = g + a
reconsider A = a, B = g as Real ;
thus a + g = B + A by BINOP_2:def 9
.= g + a by BINOP_2:def 9 ; :: thesis: verum