theorem Th47: :: GROUP_1A:248

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