theorem :: GROUP_1A:252

for G being addGroup
for a being Element of G
for A, B being Subset of G holds (A + B) * a c= (A * a) + (B * a) by Th34;