for G being Group
for H being Subgroup of G holds (carr H) * (carr H) = carr H