:: deftheorem defines * GROUP_1A:def 31 :
for G being addGroup
for A, B being Subset of G holds A * B = { (g * h) where g, h is Element of G : ( g in A & h in B ) } ;