for G being Group
for H1, H2 being Subgroup of G holds
( H1 * H2 = (carr H1) * (carr H2) & H1 * H2 = H1 * (carr H2) & H1 * H2 = (carr H1) * H2 ) ;