for G being addGroup
for a being Element of G holds ((0). G) * a = (0). G