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