Induction commutes with inflation along a normal subgroup

Since $K⊴G$ by [F6] and $K\le H\le G$, the quotient $H\mathrm{/}K$ is a group and $h\mapsto \bar{h}$ is a homomorphism $H\to \bar{H}$; hence the $H$-action on the inflated module, which is the $\bar{H}$-action through $h\mapsto \bar{h}$ by [F2], is well defined. For $\bar{f}\in {\mathrm{Infl}}_{\bar{G}}^G({\mathrm{Ind}}_{\bar{H}}^{\bar{G}}W)$ define $\mathrm{\Phi }(\bar{f}):G\to W$ by $\mathrm{\Phi }(\bar{f})(g):=\bar{f}(\bar{g})=\bar{f}(\pi (g))$. If $h\in H$, then $\pi (gh)=\bar{g}\bar{h}$ by [F3], so $\mathrm{\Phi }(\bar{f})(gh)=\bar{f}(\bar{g}\bar{h})={\bar{h}}^{-1}\cdot \bar{f}(\bar{g})=h^{-1}\cdot \mathrm{\Phi }(\bar{f})(g)$; hence $\mathrm{\Phi }(\bar{f})\in {\mathrm{Ind}}_H^G({\mathrm{Infl}}_{\bar{H}}^{H}W)$ by [F1].

$\mathrm{\Phi }$ is $\mathbb{C}$-linear, and it is injective: if $\mathrm{\Phi }(\bar{f})=0$, then $\bar{f}(\bar{g})=\mathrm{\Phi }(\bar{f})(g)=0$ for every $g\in G$, and every element of $\bar{G}$ is some $\bar{g}$ by [F3], so $\bar{f}=0$.

$\mathrm{\Phi }$ is surjective. Given $F\in {\mathrm{Ind}}_H^G({\mathrm{Infl}}_{\bar{H}}^{H}W)$, define $\bar{f}:\bar{G}\to W$ by $\bar{f}(\bar{g}):=F(g)$. This is well defined: if $\bar{g}={\bar{g}}^{\mathrm{\prime }}$, then $g^{\mathrm{\prime }}=gk$ with $k\in K\le H$ by [F3], so $F(g^{\mathrm{\prime }})=F(gk)=k^{-1}\cdot F(g)=F(g)$ by [A1] and [F2]. Moreover $\bar{f}$ is $\bar{H}$-covariant, since for $\bar{h}\in \bar{H}$ one has $\bar{f}(\bar{g}\bar{h})=F(gh)=h^{-1}\cdot F(g)={\bar{h}}^{-1}\cdot \bar{f}(\bar{g})$ for any $h\in H$ with image $\bar{h}$, so $\bar{f}\in {\mathrm{Ind}}_{\bar{H}}^{\bar{G}}W$ and $\mathrm{\Phi }(\bar{f})=F$.

$\mathrm{\Phi }$ is $G$-equivariant: for $x,g\in G$ and $\bar{f}$ as in step 1.1, $\mathrm{\Phi }(x\cdot \bar{f})(g)=(x\cdot \bar{f})(\bar{g})=\bar{f}({\bar{x}}^{-1}\bar{g})=\bar{f}(\overline{x^{-1}g})=\mathrm{\Phi }(\bar{f})(x^{-1}g)=(x\cdot \mathrm{\Phi }(\bar{f}))(g)$, using [F3] and the action rules of [F1].

Steps 2.1, 2.2 and 2.3 show that $\mathrm{\Phi }$ is a $G$-equivariant $\mathbb{C}$-linear bijection, which is the asserted isomorphism. For the final clause let $\bar{H}\le \bar{G}$, put $H={\pi }^{-1}(\bar{H})$, let $W$ be one-dimensional with ${\mathrm{Ind}}_{\bar{H}}^{\bar{G}}W$ irreducible, and note $K\le H\le G$ and $H\mathrm{/}K=\bar{H}$. By the isomorphism just proved the inflation of ${\mathrm{Ind}}_{\bar{H}}^{\bar{G}}W$ is isomorphic to ${\mathrm{Ind}}_H^G({\mathrm{Infl}}_{\bar{H}}^{H}W)$, and ${\mathrm{Infl}}_{\bar{H}}^{H}W$ is one-dimensional because it has the same underlying space as $W$ by [F2]; the inflation is irreducible because inflation preserves irreducibility in both directions by [F4] and ${\mathrm{Ind}}_{\bar{H}}^{\bar{G}}W$ is irreducible. Hence it is a monomial irreducible $G$-module induced from the one-dimensional $H$-module ${\mathrm{Infl}}_{\bar{H}}^{H}W$ by [F5].