theorem :: GROUP_1A:246

for G being addGroup
for g being Element of G
for A, B being Subset of G holds (A * g) * B = A * (g + B) by Th35;