Basic group theory question on the index of subgroups I'm doing some summer reading of Fraleigh's A First Course in Abstract Algebra and I came across this exercise in Section 10.  I'm trying to prove the following theorem and I'm wondering if I can get some feedback on my proof.  Note that $(G:H)$ refers to the index of $H$ in $G$.
Theorem: Suppose $H$ and $K$ are subgroups of the group $G$ such that $K \leq H \leq G$ and suppose that $(H:K)$ and $(G:H)$ are finite.  Then $(G:K)$ is finite and $(G:K) = (G:H) (H:K)$.  
Proof: First, define $\{a_iH | i = 1, 2, \cdots, r\}$ and $\{b_jK | j = 1, 2, \cdots s\}$ to be the collection of distinct left cosets of H in G and K in H, respectively.  Note that since (H:K) and (G:H) are finite, we know that the size of these groups are finite and $r,s < \infty$.  Then $r = (G:H)$ and $s = (H:K)$.  Note that $\cup_{j=1}^s b_jK = H$, so $\{a_iH| i = 1, 2, \cdots, r\} = \{a_i(\cup_{j=1}^s b_jK)| i = 1, 2, \cdots, r\}$.  Similarly we have that $\cup_{i=1}^r\left[a_i\left(\cup_{j=1}^s b_jK\right)\right] = G$.  Note that for each $i$, we have $a_i\left(\cup_{j=1}^s b_jK\right)$ is distinct via assumption.  Now suppose that there exists integers $1\leq m < n \leq s$ such that $a_ib_mK = a_ib_nK$.  Since $a_i \in G$ and $G$ is a group, via group cancellation law we have $b_mK = b_nK$. This is a contradiction as we assumed the left cosets of $K$ are distinct.  Thus for all $i,j$ we have $a_ib_jK$ are distinct.  Therefore, as all are distinct and $\cup_{i=1}^r\cup_{j=1}^s a_ib_jK = G$, we see that $S = \{a_ib_jK | i=1,2,\cdots, r; j=1,2,\cdots, s\}$ is the collection of distinct left cosets of $K$ in $G$ and $(G:K) = |S|$ where $|S| = rs = (G:H)(H:K)$.  Thus $(G:K)$ is finite and $(G:K)=(G:H)(H:K)$.
Any advice would be appreciated, thanks!
 A: 
First, define $\{a_iH|i=1,2,\ldots,r\}$ and $\{b_jK|j=1,2,\ldots,s\}$ to be the collection of distinct left cosets of $H$ in $G$ and $K$ in $H$, respectively. Note that since $(H:K)$ and $(G:H)$ are finite, we know that the size of these groups are finite and $r,s<\infty$. Then $r=(G:H)$ and $s=(H:K)$.

I think this is a lot more throat-clearing than you need, and depending on precisely what you mean by the middle sentence might even be wrong. It's not true that if $(G:K)$ is finite the orders of $G$ and $K$ are finite (quick counter-example: $(\mathbb{Z}:2\mathbb{Z})=2$). 
I don't know if you've reached quote groups yet, but if you did and you meant that $\lvert G/K\rvert=(G:K)$, well, you're right -- provided that $G/K$ exists, but it doesn't always exist (quick counter-example: There is no such thing as $S_3/S_2$).
All this is beside the point though, because the claim that $G$ and $K$ are finite could just as well have been omitted from your proof, and you're right to start with labelling the cosets of $K$ in $H$ and $H$ in $G$, and to stipulate $(G:H)=r$ and $(H:K)=s$.

Note that $\cup^s_{j=1}b_jK=H$, so $\{a_iH|i=1,2,⋯,r\}=\{a_i(\cup_{j=1}^sb_jK)|i=1,2,\ldots,r\}$. Similarly we have that $\cup^r_{i=1}[a_i(\cup_{j=1}^sb_jK)]=G$. Note that for each $i$, we have $a_i(\cup^s_{j=1}b_jK)$ is distinct via assumption. Now suppose that there exists integers $1\leq m<n\leq s$ such that $a_ib_mK=a_ib_nK$. Since $a_i\in G$ and $G$ is a group, via group cancellation law we have $b_mK=b_nK$. This is a contradiction as we assumed the left cosets of $K$ are distinct. Thus for all $i,j$ we have $a_ib_jK$ are distinct. Therefore, as all are distinct and $\cup^r_{i=1}\cup^s_{j=1}a_ib_jK=G$, we see that $S=\{a_ib_jK|i=1,2,\ldots,r;j=1,2,\ldots,s\}$ is the collection of distinct left cosets of $K$ in $G$ and $(G:K)=\lvert S\rvert$ where $\lvert S\rvert=rs=(G:H)(H:K)$. Thus $(G:K)$ is finite and $(G:K)=(G:H)(H:K)$.

This is correct, but as a matter of clarity I think it could benefit from more words and fewer symbols. Here's how I'd have made the same argument: 
Take $g\in G$. The cosets of $H$ partition $G$, so we know $g$ is in exactly one of them, call it $a_iH$. To put $g\in a_iH$ another way, we might say there's some $h\in H$ satisfying $g=a_ih$. We can repeat this exact same argument with $h$ and $K$ partitioning $H$ to get $g\in a_i(b_jK)=(a_ib_j)K$. We have now put each element of $G$ in exactly one of the cosets $\{a_ib_jK|1\leq i\leq r,1\leq j\leq s\}$. Now $$\lvert\{a_ib_jK|1\leq i\leq r,1\leq j\leq s\}\rvert=rs\text,$$ so $(G:K)=rs=(G:H)(H:K)$ and is finite.
