theorem :: GROUP_1A:239

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