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