theorem :: GROUP_1A:250

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