theorem :: GROUP_1A:247

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