:: deftheorem defines * GROUP_2:def 13 :
for G being Group
for H being Subgroup of G
for a being Element of G holds a * H = a * (carr H);