Regarding Lemma 21.9 of Jech

Jech states the following lemma in his book:

Lemma 21.9 Let $j:Vto M=operatorname{Ult}_U(V)$ be an elementary embedding with a critical point $kappa$. If $mathbb{P}in M$ is a forcing poset such that $|mathbb{P}|lekappa$ and $G$ is a $V$-generic filter over $mathbb{P}$, then $M[G]$ is closed under $kappa$-sequences. (i.e., $({^kappa}M[G])^{V[G]}subseteq M[G]$.)

(The original statement involves with $lambda$-supercompactness, and states $M[G]$ is closed under $lambda$-sequences under the hypothesis $|mathbb{P}|lelambda$. I will only consider the measurable case for simplicity.)

He starts with the proof as follows:

It suffices to show that if $fin V[G]$ is a function from $kappa$ into ordinals, then $fin M[G]$. (…)

I do not understand this point. I can see that if $M[G]$ is closed under functions $kappato mathrm{Ord}$, then the standard Mostowski argument with some coding shows $M[G]$ is closed under functions from $kappa$ to $H_{kappa^+}^{V[G]}$. Hence I tried to prove it in another way:

My attempt. Let $fin V[G]$, $f:kappato M[G]$. Take $p_0in G$ such that $p_0Vdash dot{f}text{ is a function from $kappa$ to $M^mathbb{P}$}.$
For each $alpha<kappa$, take
$$A_alpha := {ple p_0mid exists sigmain M^mathbb{P}[pVdash dot{f}(alpha)=sigma]}.$$
For each $alpha<kappa$ and $pin A_alpha$, choose $sigma_{alpha,p}in M^mathbb{P}$ that witnesses $pin A_alpha$. Since the choice is made over $V$, $langle sigma_{alpha,p}midalpha,pranglein V$.
Furthermore, we can choose $g_{alpha,p}:kappato V$ such that $sigma_{alpha,p}=[g_{alpha,p}]_U$.

Now define a function $g_p$ as $$g_p(alpha)(xi) := g_{alpha,p}(xi)$$
if it is defined. Then $g_p$ sends $xi$ to a partial function over $kappa$.
Take $h_p=[g_p]_Uin M$. Then $M$ thinks $h_p$ is a partial function from $j(kappa)$ to $M^mathbb{P}$. Moreover, we have

• $p’le pimplies operatorname{dom} h_psubseteq operatorname{dom} h_{p’}$, and
• $p’le p implies p’Vdash h_p(alpha)=h_{p’}(alpha)$ (Here $h_p(alpha)$ and $h_{p’}(alpha)$ themselves are treated as a single $M^mathbb{P}$-name.)

Let $h(alpha):= h_p(alpha)$ for some $p$. Then $h$ is a partial function from $j(kappa)$. Since $A_alphacap G$ is nonempty for each $alpha$, $h_p(alpha)$ is defined for all $alpha<kappa$. Moreover, by definition of $A_alpha$, we have $f(alpha)=h(alpha)$ for $alpha<kappa$. Hence $f=hupharpoonright kappain M[G]$.

My questions are as follows:

1. Why just showing $({^kappa}mathrm{Ord})^{V[G]}subseteq M[G]$ suffices to prove Lemma 21.9?
2. Is my argument correct?

Thank you for any help in advance.