[step:Construct a bijection between $W_k(x, y)$ and walks of length $k-1$ ending at a neighbour of $y$]Consider the map
\begin{align*}
\Phi: W_k(x, y) &\to \bigsqcup_{\substack{z \in V(G) \\ z \sim y}} W_{k-1}(x, z) \\
(v_0, v_1, \ldots, v_{k-1}, v_k) &\mapsto (v_0, v_1, \ldots, v_{k-1}),
\end{align*}
which removes the final vertex. We verify $\Phi$ is well-defined and bijective.
*Well-defined.* Given a walk $w = (v_0, \ldots, v_k) \in W_k(x, y)$, its truncation $\Phi(w) = (v_0, \ldots, v_{k-1})$ is a sequence with $v_0 = x$ and consecutive vertices adjacent (inherited from $w$). Setting $z := v_{k-1}$, the walk condition at the final step gives $v_{k-1} \sim v_k$, i.e., $z \sim y$. Hence $\Phi(w) \in W_{k-1}(x, z)$ with $z \sim y$, so $\Phi(w)$ lies in the target disjoint union.
*Injective.* If $\Phi(w) = \Phi(w')$ for $w = (v_0, \ldots, v_k)$ and $w' = (v'_0, \ldots, v'_k)$, then $v_i = v'_i$ for $i = 0, \ldots, k-1$; and $v_k = y = v'_k$ by the definition of $W_k(x, y)$. So $w = w'$.
*Surjective.* Given $z \sim y$ and a walk $(v_0, \ldots, v_{k-1}) \in W_{k-1}(x, z)$, the extended sequence $(v_0, \ldots, v_{k-1}, y)$ satisfies $v_0 = x$, $v_k := y = y$, and the adjacency conditions $v_{i-1} \sim v_i$ for $i = 1, \ldots, k - 1$ (inherited) and $v_{k-1} = z \sim y$ (by hypothesis). Hence it lies in $W_k(x, y)$ and maps to the given walk under $\Phi$.
Therefore
\begin{align*}
|W_k(x, y)| = \sum_{\substack{z \in V(G) \\ z \sim y}} |W_{k-1}(x, z)|.
\end{align*}[/step]