for G being non empty addGroup-like addMagma
for g being Element of G
for A being Subset of G st G is Abelian addGroup holds
g + A = A + g by Th25;