Solution (source code)

= Solution

Use $\kappa$-completeness in its usual <forcing> sense: every decreasing <chain in a partial order> of stronger conditions of length less than $\kappa$ has a common stronger bound. Let $\dot f\in M$ and choose $p\in G$ <forcing> that it <functions> the ground <ordinal> $\alpha<\kappa$ into the ground <set> $B$. Below any stronger condition $r$, recursively decide each value of $\dot f$ in order. At a successor step the deciding conditions are dense, and at a limit stage use $\kappa$-completeness. After all $\alpha$ steps take another common bound. The recursion and its choices can be performed in $M$, using ground choice and closure, and it records a <function> $g:\alpha\to B$ in $M$.

Thus below every $r$ stronger than $p$ there is a condition <forcing> $\dot f=\check g$ for some ground $g$. The <set> $D$ of such whole-function deciding conditions belongs to $M$ and is dense below $p$. Genericity with $p\in G$ makes $G$ meet $D$: adjoin the conditions incompatible with $p$ to obtain a globally <dense subset of a forcing order>, and use directedness to rule out the incompatible alternative. A condition in $G\cap D$ then gives $f=g\in M$.

The reverse inclusion follows because ground <functions> remain <functions> with the same domain and values. Therefore
$$
\boxed{({}^\alpha B)^M=({}^\alpha B)^{M[G]}.}
$$
This <closed forcing adds no short ground-valued sequences> argument needs density of complete decisions. A single arbitrarily constructed lower bound need not belong to $G$, and would not by itself prove the claim.