theorem :: GROUP_1A:240

for G being addGroup
for a, b, c being Element of G holds {a,b} * {c} = {(a * c),(b * c)}