for G being addGroup
for g being Element of G
for A being Subset of G holds A * g = ((- g) + A) + g