In the following, we apply the two important facts
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$