theorem ThB16: :: GROUP_1A:217

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