Mackey's double-coset formula for restricting an induced character

Let $I={\mathrm{Ind}}_H^{G}W$. For each $s\in S$, let $I_s$ be the subspace of functions in $I$ whose support is contained in the double coset $KsH$. Because the double cosets $KsH$ partition $G$, every induced function splits uniquely as the sum of its restrictions to those supports, so ${\mathrm{Res}}_K^{G}I={⨁}_{s\in S}{I}_s$ as $K$-modules.

For $s\in S$, define ${\mathrm{\Theta }}_s:I_s\to {\mathrm{Ind}}_{K\cap sH{s}^{-1}}^K({\mathrm{Res}}_{K\cap sH{s}^{-1}}^{sH{s}^{-1}}{}^{s}W)$ by ${\mathrm{\Theta }}_s(f)(k):=f(ks)$. If $u\in K\cap sH{s}^{-1}$ and $u=sh{s}^{-1}$, then ${\mathrm{\Theta }}_s(f)(ku)=f(ksh)=h^{-1}\cdot f(ks)=u^{-1}\cdot {\mathrm{\Theta }}_s(f)(k)$, where the last action is that of ${}^{s}W$ from [F3]. So ${\mathrm{\Theta }}_s(f)$ is well defined in the target induced module.

For $\phi \in {\mathrm{Ind}}_{K\cap sH{s}^{-1}}^K({\mathrm{Res}}_{K\cap sH{s}^{-1}}^{sH{s}^{-1}}{}^{s}W)$, define $f_{\phi }:G\to W$ by $f_{\phi }(ksh):=h^{-1}\cdot \phi (k)$ on $KsH$ and $f_{\phi }(g):=0$ off $KsH$. If $ksh=k^{\mathrm{\prime }}s{h}^{\mathrm{\prime }}$, then $k^{-1}{k}^{\mathrm{\prime }}=sh{h}^{\mathrm{\prime }-1}{s}^{-1}\in K\cap sH{s}^{-1}$, and the covariance condition in the target induced module gives $h^{-1}\cdot \phi (k)=h^{\mathrm{\prime }-1}\cdot \phi (k^{\mathrm{\prime }})$. Thus $f_{\phi }$ is well defined, lies in $I_s$, and inverts ${\mathrm{\Theta }}_s$.

Steps 2.1 and 3.1 show that ${\mathrm{\Theta }}_s$ is a $K$-equivariant isomorphism $I_s\cong {\mathrm{Ind}}_{K\cap sH{s}^{-1}}^K({\mathrm{Res}}_{K\cap sH{s}^{-1}}^{sH{s}^{-1}}{}^{s}W)$ for each $s\in S$. Combining these isomorphisms with step 1.1 gives a $K$-module decomposition of ${\mathrm{Res}}_K^{G}I$ as the direct sum of the stated induced modules.

Taking characters of the $K$-module decomposition in step 4.1 and using [F1] yields the stated Mackey double-coset formula.