I want to be completely certain that I understand the last assertion of the "correspondence" theorem in Artin's book. The theorem, slightly paraphrased, is:
Let $\varphi: G \to \mathcal{G}$ be a surjective group homomorphism with kernel $K$. There is a bijective correspondence between subgroups of $\mathcal{G}$ and subgroups of $G$ that contain $K$. If $H$ and $\mathcal{H}$ are corresponding subgroups, then $H$ is normal in $G$ if and only if $\mathcal{H}$ is normal in $\mathcal{G}$. If $H$ and $\mathcal{H}$ are corresponding subgroups, then $|H| = |\mathcal{H}||K|$.
The only thing I'm uncertain about is the final statement. After much thinking, I believe this is using the "counting formula." We have a homomorphism $\varphi: G \to \mathcal{G}$ and, earlier in the proof, establish that $\varphi^{-1} (\mathcal{H})$ is a subgroup containing $K$, so we can restrict $\varphi$ to $\varphi^{-1} (\mathcal{H}) \subset G$ and still have a homomorphism. By the counting formula, we have $$ |\varphi^{-1} (\mathcal{H})| = |\text{Image}(\varphi^{-1} (\mathcal{H}))| \cdot |\text{Kernel}(\varphi^{-1} (\mathcal{H}))|. $$ Because $\varphi$ is surjective, we have $\varphi(\varphi^{-1} (\mathcal{H})) = \mathcal{H}$. As $\varphi^{-1} (\mathcal{H})$ contains the kernel $K$, its kernel is likewise $K$, so $$ |\varphi^{-1} (\mathcal{H})| = |\mathcal{H}| \cdot |K|. $$ Finally, we have $\varphi^{-1} (\mathcal{H}) = H$ by definition, which gives the result.
Is this reasoning correct?