:: deftheorem defines * GROUP_9:def 24 :
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 * H2 = (carr H1) * (carr H2);