theorem Th22: :: GROUP_1A:223

for G being addGroup
for a, b being Element of G holds
( a * b = a iff a + b = b + a )