Induction commutes with an external tensor factor

Since $C\le P$ and $D\le Q$, the componentwise product $C\times D$ contains the identity and is closed under products and inverses in $P\times Q$, so it is a subgroup. The basis inclusion $\mathbb{C}[C\times D]\hookrightarrow \mathbb{C}[P\times Q]$ respects multiplication, giving the right subgroup-ring action used below. All three group indices are finite.

On group-basis and module generators define $\mathrm{\Phi }([(p,q)]\otimes (x\otimes y)):=([p]\otimes x)\otimes ([q]\otimes y)$. For fixed $(p,q)$, the formula is complex-bilinear in $x,y$, so it descends to $X{\otimes }_{\mathbb{C}}Y$. For $(c,d)\in C\times D$, the images of $[(pc,qd)]\otimes (x\otimes y)$ and $[(p,q)]\otimes (cx\otimes dy)$ both equal $([p]\otimes cx)\otimes ([q]\otimes dy)$. Thus the pairing is balanced over $\mathbb{C}[C\times D]$, and [F4] gives a well-defined map on the source tensor product.

Define $\mathrm{\Psi }(([p]\otimes x)\otimes ([q]\otimes y)):=[(p,q)]\otimes (x\otimes y)$. Moving $c\in C$ across the first factor preserves its value because $[(pc,q)]=[(p,q)(c,1)]$ and the balanced relation moves $(c,1)$ to the action $cx$; the same check with $d\in D$ uses $[(p,qd)]=[(p,q)(1,d)]$. The formula is complex-bilinear in the two outer factors, so [F4] gives a well-defined reverse map.

The finite group rings in [F3] have finite bases, so their tensor models on the finite-dimensional inputs [F8] are finite-dimensional. Apply [F2] with $R=\mathbb{C}$ to the subgroup inclusions $C\times D\le P\times Q$, $C\le P$, and $D\le Q$; it identifies the induction terms with the group-ring tensor models used above.

The composites $\mathrm{\Psi }\mathrm{\Phi }$ and $\mathrm{\Phi }\mathrm{\Psi }$ fix every displayed group-basis and pure-tensor generator. These generators span their respective tensor products by [F3, F4], so the composites are identity maps and $\mathrm{\Phi }$ is an isomorphism.

Left multiplication by $(p_0,q_0)$ sends $[(p,q)]$ to $[(p_{0}p,q_{0}q)]$, which $\mathrm{\Phi }$ sends to the corresponding left actions on both target factors. The same formula commutes with $C$- and $D$-module homomorphisms on $X,Y$, so the isomorphism is $(P\times Q)$-equivariant and natural.

The tensor-model identifications in step 2.1 turn $\mathrm{\Phi }$ into the module isomorphism in (i). If $D=Q$, the canonical map $\mathbb{C}[Q]{\otimes }_{\mathbb{C}[Q]}Y\to Y$, $[q]\otimes y\mapsto qy$, is an isomorphism with inverse $y\mapsto [e_Q]\otimes y$; if also $C=P$, the same identity gives ${\mathrm{Ind}}_P^{P}X\cong X$. Thus (ii) holds.

Since $X,Y$ are finite-dimensional [F8] and the finite group rings in [F3] have finite bases, the tensor models of step 2.1 are finite-dimensional and have characters. Taking characters of the isomorphism in step 3.1 and applying [F6] to the two representations pulled back along the coordinate projections of $P\times Q$ gives the stated identity in $R(P\times Q)$ by [F7] and [F9]. All maps were defined explicitly, so no choice principle is used.