:: deftheorem defines * GROUP_2:def 4 :
for G being non empty multMagma
for g being Element of G
for A being Subset of G holds A * g = A * {g};