Solution (source code)

= Solution

Let $G$ have a <generating set of a group> with $r$ elements. Every subgroup $H$ of index $n$ gives a <transitive group action> of $G$ on the $n$ left cosets of $H$, hence a <group homomorphism> $\rho_H:G\to S_n$ after the cosets are labelled. Conversely, $H$ is the <stabilizer subgroup> of one point in this action.

A homomorphism $G\to S_n$ is determined by the images of the $r$ generators, so there are at most $(n!)^r$ such homomorphisms and at most $n(n!)^r$ point stabilizers. Therefore the <finiteness of subgroups of a fixed finite index> gives \b[only finitely many subgroups of index $n$].