theorem Th50: :: GROUP_1A:251

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