for G being addGroup
for a being Element of G holds
( ((0). G) + a = {a} & a + ((0). G) = {a} )