[proof] Write $V = \operatorname{Ind}_H^G W$. Fix a left transversal $\mathcal{T}$ of $H$ in $G$, so that $V = \bigoplus_{t \in \mathcal{T}} t \otimes W$ as vector spaces. The key idea is to coarsen this decomposition by grouping together the summands $t \otimes W$ according to which double coset $KgH$ the element $t$ belongs to. For each $g \in \mathcal{S}$, define \begin{align*} V(g) = \bigoplus_{t \in KgH \cap \mathcal{T}} t \otimes W. \end{align*} Step 1: Show each $V(g)$ is a $K$-subspace. For $k \in K$ and $t \in KgH \cap \mathcal{T}$, we have $kt \in KgH$, so there exists $t' \in \mathcal{T}$ with $t'H = ktH$ and $t' \in KgH$. The action is $k \cdot (t \otimes w) = t' \otimes \rho(t'^{-1}kt)w$, which stays in $V(g)$. Step 2: As a $K$-space, $\operatorname{Res}_K^G V = \bigoplus_{g \in \mathcal{S}} V(g)$, since the double cosets partition $G$ and the transversal elements distribute accordingly. Step 3: Show $V(g) \cong \operatorname{Ind}_{H_g}^K W_g$ as $K$-representations. Elements $t \in KgH \cap \mathcal{T}$ correspond to cosets $kgH$ for $k \in K$, and the cosets $kgH$ are in bijection with elements of $K/H_g$ (via $k \mapsto k$ modulo $H_g = gHg^{-1} \cap K$). So \begin{align*} V(g) = \bigoplus_{k \in K/H_g} (kg) \otimes W. \end{align*} Define the map $\operatorname{Ind}_{H_g}^K W_g \to V(g)$ by $k \otimes w \mapsto kg \otimes w$. This is an isomorphism of vector spaces. To verify $K$-equivariance: for $x \in K$, acting on $k \otimes w$ in $\operatorname{Ind}_{H_g}^K W_g$ gives $k' \otimes \rho_g(k'^{-1}xk)w = k' \otimes \rho(g^{-1}k'^{-1}xkg)w$ for the unique $k' \in K$ with $k'^{-1}xk \in H_g$. Acting on $kg \otimes w$ in $V(g)$ gives $k''g \otimes \rho(g^{-1}k''^{-1}xkg)w$ for the unique $k''$ with $k''^{-1}xkg \in H$; by uniqueness of the transversal representative, $k'' = k'$. So the two actions match under the map, establishing the isomorphism. Combining Steps 2 and 3 gives the result. [/proof]