Checking well definedness of bijection from $G/H \times H/K$ to $G/K$ For the sequence of subgroups$$K \leq H\leq G$$
I am trying to create a bijection $\phi:G/H\times H/K \rightarrow G/K$ defined by $$\phi(gH, hK) = (gh)K$$
I can show injectivity since $e\in G/K$ is $K$ and for any two elements $(gh)K = K$ iff $gh\in K$. I am stuck here in showing that $g, h\in K$. Then $h\in K$ and since $K\leq H$, then $g\in H$, so clearly $(gH, hK) = (eH, eK)$. 
For sujectivity I have that for any $s\in G$ $$\phi(eH, sK) = (es)K = sK$$
The problem that I am struggling with is to show that $\phi$ is a well defined function when we only have the subgroup relation. 
Let $g_1H = g_2H$ and $h_1K = h_2K$ so then we have that $g_2^{-1}g_1\in H$ and $h_2^{-1}h_1\in K$. So $$\phi((g_2^{-1}g_1)H, (h_2^{-1}h_1)K) = \phi(eH, e K) = eK$$ $$\phi((g_2^{-1}g_1)H, (h_2^{-1}h_1)K) = (g_2^{-1}g_1h_2^{-1}h_1)K$$
Thus 
$$(g_2^{-1}g_1h_2^{-1}h_1)K = eK$$
This is where I am getting stuck, I may be using the wrong function.
 A: The function $\phi$ is not necessarily injective.  Consider $G:=A_4$ the $4$-th alternating group, $H:=V$ is the unique nontrivial proper normal subgroup of $G$, and $K:=\big\langle (1\;2)(3\;4)\big\rangle\cong C_2$.  Here, for each $n\in\mathbb{Z}_{>0}$, $C_n$ denotes the cyclic group of order $n$.  Note that $V$ is isomorphic to $C_2\times C_2$.
Take $g_1:=(1\;2\;3)\in G$, $g_2:=(2\;4\;3)\in G$, $h_1:=(1\;3)(2\;4)\in H$, and $h_2:=()\in H$.  Then, $g_1h_1=g_2=g_2h_2$, whence
$$\phi(g_1H,h_1K)=(g_1h_1)K=(g_2h_2)K=\phi(g_2H,h_2K)\,.$$
In fact, $\phi$ is not even well defined.  Observe that $g_1^{-1}g_2=h_1\in H$, so $g_1H=g_2H$.  However,
$$\phi(g_1H,h_2K)=(g_1h_2)K=g_1K=\big\{(1\;2\;3),(1\;3\;4)\big\}$$
and
$$\phi(g_2H,h_2K)=(g_2h_2)K=g_2K=\big\{(2\;4\;3),(1\;4\;2)\big\}\,,$$
so $$\phi(g_1H,h_2K)\neq \phi(g_2H,h_2K)$$ despite $g_1H=g_2H$ and $h_2K=h_2K$.

If the goal is to prove that
$$[G:K]=[G:H]\,[H:K]\,,$$
then there is a different way to do the job.  Let $f:(G/K)\to (G/H)$ be the function given by $$f(gK):=gH\text{ for all }g\in G\,.$$
This is a well defined function.  Fix a set of representatives $\left\{g_\alpha\right\}_{\alpha \in J}\subseteq G$ of $G/H$ for some index set $J$.  For a given $\alpha \in J$, the fiber of $g_\alpha H \in G/H$ is the set $$S_\alpha:=f^{-1}(g_\alpha H)=\big\{\gamma K\in G/K\,\big|\,\gamma H= g_\alpha H\big\}\,.$$
Let $F_\alpha:S_\alpha\to H/K$ to be the function taking
$$\gamma K\mapsto g_\alpha^{-1}\gamma K\,.$$
Observe that $F_{\alpha}$ is a well defined bijection.  This proves that 
$$\begin{align}[G:K]&=|G/K|=\left|\bigcup_{\alpha\in H}\,\{\alpha\}\times S_\alpha\right|\\&=\left|\bigcup_{\alpha\in J}\,\{\alpha\}\times (H/K)\right|=|J|\, |H/K|\\&=|G/H|\,|H/ K|=[G:H]\,[H:K]\,.\end{align}$$

Well, I just realized that you can fix the function $\phi$ by defining it as $\phi:J\times (H/ K)\to (G/K)$ instead.  (Fix a set of representatives $\left\{g_\alpha\right\}_{\alpha \in J}\subseteq G$ of $G/H$ for some index set $J$, as before.)  That is, you take
$$\phi(\alpha,h K):=g_\alpha h K$$
for all $\alpha\in J$ and $h K\in (H/K)$.  You now have a well defined bijection.
