Green distinguished summands are mutually inverse

By F1, $M\mid {\mathrm{Ind}}_H^{G}f(M)$. Applying F2 to $f(M)$ gives exactly one summand with vertex in $\mathcal{Z}$, namely $g(f(M))$. The module $M$ is indecomposable with such a vertex, and F3 excludes it from the exceptional part. Comparing indecomposable multiplicities by F4 forces $M\cong g(f(M))$. The use of F1, F2 and F4 carries the assumed AC.

Conversely, F2 gives $U\mid {\mathrm{Res}}_H^{G}g(U)$. By F1 this restriction has exactly one admissible indecomposable summand, $f(g(U))$. Since $U$ is admissible and F3 excludes it from the error, F4 gives $U\cong f(g(U))$.

An isomorphism of $G$-modules restricts to an $H$-isomorphism. An $H$-isomorphism $a:U\to U^{\mathrm{\prime }}$ induces an isomorphism $x\otimes u\mapsto x\otimes a(u)$, with inverse induced by $a^{-1}$. Thus each functor preserves the whole module isomorphism class. By F1, F2 and F4 its unique admissible summand has an isomorphism class independent of every chosen decomposition. Hence both assignments descend to isomorphism classes and 1.1–1.2 make them inverse there.

If $H=G$, both functors and assignments are identities on the stated domain and both errors are zero. If $P=1$, the normalizer hypothesis forces $H=G$. Zero modules are not indecomposable inputs. No canonical vector-space representatives or simultaneous choices of representatives of all isomorphism classes are needed: uniqueness defines the maps on classes. This proves the assertion with precisely the inherited AC assumption. [F1, F2, step 2.1] QED