Evaluation at 1 commutes with the cup cochain on coinduced modules

Let $k$ be a commutative ring, $G$ a group and $S \le G$ a subgroup, and let $A$, $B$, $N$ be $k$-linear representations of $S$. Let $\varphi \colon A \to_{k} (B \to_{k} N)$ be a $k$-bilinear map (no equivariance is assumed). Let $x \colon G \to \mathrm{coind}_{S\hookrightarrow G} A$ and $y \colon G \to \mathrm{coind}_{S \hookrightarrow G} B$ be arbitrary functions into the representations coinduced along the inclusion $S \hookrightarrow G$, whose underlying objects consist of functions $f \colon G \to A$ (resp. $G \to B$) satisfying the $S$-equivariance condition, with $G$ acting by right translation, and let $s, t \in S$. The assertion is that

where, by definition of cupCochain, the right-hand side is $\varphi\bigl(x(s)(1)\bigr)\bigl(B.\rho\,s\,(y(t)(1))\bigr)$, the bidegree-$(1,1)$ cup-product cochain formed over $S$ from the two evaluated-at-$1$ functions $S \to A$ and $S \to B$.

This is the cochain-level compatibility of the cup product with the map "restrict to $S$ and evaluate at $1$" underlying Shapiro's lemma $H^i(G, \mathrm{coind}_S^G X) \cong H^i(S, X)$, in bidegree $(1,1)$. It is used in the proof of groupCohomology.bijective_theta_coind.