theorem :: GROUP_1A:249

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