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