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