This fact is used in the proof of the Theorem on Functional Extensions in J.R. Shoenfield's Mathematical Logic.
Let $x, y_1, ..., y_n$ be distinct variables, $A$ - some formula in which no variable other than $x, y_1, ..., y_n$ is free, $B$ - some closed formula, and $f$ - a new $n$-ary functional symbol.
If $C$ is a prenex form of $A\to B$, then $\exists y_1...\exists y_nC_x[fy_1...y_n]$ is a prenex form of $\forall y_1...\forall y_n A_x[fy_1...y_n]\to B$.
The way it is mentioned in the proof makes me feel like this should be trivial but I still can't see why the statement is true.
P.S. I think I provided enough details to prove the statement but I am not sure. I will provide the whole proof if necessary.
Edit: In the book $B$ is a prenex form of $A$ iff $B$ is in prenex form and $A$ can be converted to $B$ by using only prenex operations:
1) Replace a part $\exists x C$ by $\exists yC_x[y]$, provided $y$ is not free in $C$.
2) Replace a part $\neg \exists xC$ by $\forall x\neg C$ or $\neg \forall xC$ by $\exists x\neg C$
3) Replace a part $\exists x C\vee D$ by $\exists x (C\vee D)$ or $\forall x C\vee D$ by $\forall x(C\vee D)$, provided $x$ is not free in $D$
4) Replace a part $C\vee \exists x D$ by $\exists x (C\vee D)$ or $C\vee \forall x D$ by $\forall x(C\vee D)$, provided $x$ is not free in $C$.