:: deftheorem defines * GROUP_4:def 8 :
for G being Group
for H1, H2 being Subgroup of G holds H1 * H2 = (carr H1) * (carr H2);