:: deftheorem defines * GROUP_1A:def 33 :
for G being addGroup
for A being Subset of G
for g being Element of G holds g * A = {g} * A;