Let $f : \mathbb{N}^k \to \mathbb{N}$ be a computable total function such that $f (\vec{x}) > \max \vec{x}$ for all $\vec{x}$.
Question. Why is there a decidable set $A$ such that $\operatorname{im} {\left. f \right|_{A^k}} = \mathbb{N} \setminus A$?
It feels like there should be an inductive process which gives the solution. Let $A_0 = \mathbb{N} \setminus {\operatorname{im} f}$. If there is such an $A$, then $A_0 \subseteq A$ for sure. Let for each natural number $n$, let $B_n = \mathbb{N} \setminus {\operatorname{im} f \big|_{{A_n}^k}}$ and $A_{n+1} = \mathbb{N} \setminus {\operatorname{im} f \big|_{{B_n}^k}}$. One can then show inductively that $A_0 \subseteq A_1 \subseteq A_2 \subseteq \cdots \subseteq B_2 \subseteq B_1 \subseteq B_0$ Let $A = \bigcup_n A_n$ and $B_\infty = \bigcap_n B_n$. If $\vec{x} \in A^k$, then $\vec{x} \in {A_n}^k$ for some $n$, so $f (\vec{x}) \notin B_n$, hence $\vec{x} \notin B$. On the other hand, if $y \notin B$, then $y \notin B_n$ for some $n$, so there is some $\vec{x} \in {A_n}^k$ such that $f (\vec{x}) = y$, and $\vec{x} \in A^k$. Thus $\operatorname{im} f \big|_{A^k} = \mathbb{N} \setminus B$. So far so good.
Under the hypothesis, it's easy to see that $f$ maps decidable subsets of $\mathbb{N}^k$ to decidable subsets of $\mathbb{N}$. Thus, $A$ is semidecidable, and $B$ is co-semidecidable. If $A = B$ then it follows that $A$ is decidable... but is it true that $A = B$?