for G being addGroup
for a, b being Element of G st a * b = 0_ G holds
a = 0_ G