ThmDex – An index of mathematical definitions, results, and conjectures.
Proof P665 on R468: Lagrange's theorem
P665
In the following, we apply the two important facts
(i) R643: Order of left coset modulo subgroup equals order of subgroup
(ii) R724: Set of left cosets partitions group

Since $G / H$ partitions $G$ it is, particularly, a set cover for $G$. That is, $G = \bigcup G / H$. Thus, using the fact that the order of each element of $G / H$ coincides with the order of $H$, we have \begin{equation} |G| = \left| \bigcup G / H \right| = \sum_{C \in G / H} |C| = \sum_{C \in G / H} |H| = |G / H| |H| \end{equation} Result R852: Group is not empty guarantees that $|H| \geq 1$. Thus, dividing each side by the nonzero integer $|H|$ then yields $|G / H| = |G| / |H|$. $\square$