for H, K being finite Group holds card (product <*H,K*>) = (card H) * (card K)