let G be addGroup; :: thesis: (0). G is Abelian
let a, b be Element of ((0). G); :: according to RLVECT_1:def 2 :: thesis: a + b = b + a
a in the carrier of ((0). G) ;
then a in {(0_ G)} by Def7;
then A1: a = 0_ G by TARSKI:def 1;
b in the carrier of ((0). G) ;
then b in {(0_ G)} by Def7;
hence a + b = b + a by A1, TARSKI:def 1; :: thesis: verum