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