for S being non empty addMagma st ( for r, s, t being Element of S holds (r + s) + t = r + (s + t) ) & ex t being Element of S st
for s1 being Element of S holds
( s1 + t = s1 & t + s1 = s1 & ex s2 being Element of S st
( s1 + s2 = t & s2 + s1 = t ) ) holds
S is addGroup by Def2, RLVECT_1:def 3;