"Let $\Bbb N =\{1,2,3,\cdots\}$ be the set of natural numbers and $I_n = \{1,\cdots,n\}$."
The only thing I'd do differently, here, is to point out that we're defining $I_n$ for all $n\in\Bbb N.$ I might also define $I_n=\{k\in\Bbb N\mid k\le n\},$ for precision.
'Let $X^{<\omega} = \{h: I_k \to X \mid k \in \Bbb N\}$ be the set of all finite sequences from $X$. Consider
$$\begin
{array}{l|rcl}
H : & X^{<\omega}
& \longrightarrow & X^{<\omega} \\
& h & \longmapsto & H(h) \end{array}$$
where $h: I_k \to X$.
"$H(h):I_{k+1} \to X$ is defined by $${H(h)\restriction}_{I_k} = h \text{ and } H(h)(k+1)=f_{k+1}(t)$$ where $t = \min \{n \in \mathbb N \mid f_{k+1}(n) \notin \operatorname{ran}h\}$.
"Because $|\operatorname{ran}f_{k+1}| = k+1 > |\operatorname{ran}h| = k$, $\{n \in \mathbb N \mid f_{k+1}(n) \notin \operatorname{ran}h\} \neq \emptyset$ and consequently such $t$ does exists by the fact that $\Bbb N$ is well-ordered with respect to <."
The flow here is a bit disjointed, though you seem to have the right idea. There is one error that you made: we cannot say for sure that $\lvert\operatorname{ran}h\rvert=k,$ only that $\lvert\operatorname{ran}h\rvert\leq k.$ Can you see why? Instead, I'd proceed as follows:
Given sets $A,B$ we denote the set of functions from $A$ into $B$ by ${}^AB.$ Let $X^{<\omega}=\bigcup_{k\in\Bbb N}{}^{I_k}X$ be the set of all finite sequences of elements of $X.$ We define the function $H:X^{<\omega}\to X^{<\omega}$ as follows:
For any $h\in X^{<\omega},$ there is a unique $k\in\Bbb N$ such that $h:I_k\to X.$ Observe that $$\left\lvert\operatorname{ran}f_{k+1}\right\rvert=k+1>k=\lvert\operatorname{dom}h\rvert\geq\lvert\operatorname{ran}h\rvert,$$ so we cannot have $\operatorname{ran}f_{k+1}\subseteq\operatorname{ran}h.$ Consequently, the set $\bigl\{n\in\Bbb N\mid f_{k+1}(n)\notin\operatorname{ran}h\bigr\}$ is non-empty, so has a least element--say $t_h$--since $\Bbb N$ is well-ordered. Then, we define $H(h):I_{k+1}\to X$ by $$H(h)\restriction_{I_k}=h\;\textrm{and}\;\bigl(H(h)\bigr)(k+1)=f_{k+1}(t_h).$$ Thus, $H(h)\in{}^{I_{k+1}}X\subset X^{<\omega}.$
Notice that I've also adjusted the notation slightly in the definition line (I'll address that again, shortly.) Now, let's get back to your proof.
"By Recursion Theorem, there exists a unique mapping $g:\Bbb N \to X^{<\omega}$ such that $g_1=f_1$ and $g_{n+1}=H \circ g_n$."
"Notice that $H \circ g_n (k):=(H(g_n))(k)$, i.e. $H \circ g_n (k)$ denotes the value of function $H (g_n)$ at $k$ for $k \in \operatorname{dom}H (g_n)$."
One thing I'd do differently is add "for all $n\in\Bbb N$" at the end of the first sentence. For another thing, you've gone from using the notation $H(h)(k)$ to $H\circ h(k).$ While they are effectively the same in this case, it necessitates your next comment to try to avoid confusion. But there, you compare it to the notation $\bigl(H(h)\bigr)(k),$ instead! I would instead stick with the clearest notation throughout, at which point the second sentence here becomes unnecessary. One other thing I'd add, here, is that $g_n:I_n\to X$ for all $n\in\Bbb N,$ which readily follows inductively from prior discussion during the definition of $H.$
"1. $g_n \subseteq g_{n+1}$
"By definition, $g_{n+1} = H \circ g_n$, then $g_{n+1}(i)=g_n(i)$ for all $i \in \operatorname{dom}g_n$. Hence $g_n \subseteq g_{n+1}$.
It would probably be more straightforward (if you've proved that $g_n:I_n\to X$ for all $n\in\Bbb N$) to say: "Since $g_{n+1}\restriction_{I_n}=g_n$ for all $n\in\Bbb N,$ then $g_n\subseteq g_{n+1}$ for all $n\in\Bbb N.$"
"2. $g_n$ is injective
"We prove this statement by induction on $n$. It's clear that $g_1=f_1$ is injective since $|\operatorname{dom}f_1|=1$. Assume that $g_n$ is injective for $n=k$.
"Assume the contrary that $g_{n+1}$ is not injective, then $g_{n+1}(i_1)=g_{n+1}(i_2)$ for some $i_1 < i_2 \le n+1$ or equivalently $H \circ g_n(i_1) = H \circ g_n(i_2)$ for some $i_1 < i_2 \le n+1$.
"a. If $i_2 = n+1$. Then $H \circ g_n(i_2)=H \circ g_n(i_1) =g_n(i_1)$. Thus $H \circ g_n(n+1)=H \circ g_n(i_2) =g_n(i_1) \in \operatorname{ran}g_n$. This contradicts the definition of $H \circ g_n(n+1)$.
"b. If $i_2 < n+1$. Then $i_1,i_2 \in \operatorname{dom}g_n$, then $H \circ g_n(i_1) = H \circ g_n(i_2)$ $\implies g_n(i_1)=g_n(i_2)$. This contradicts the inductive hypothesis that $g_n$ is injective.
"Hence $g_{n+1}$ is injective."
This part is much more complicated than it needs to be (and may not even be correct; I haven't read through it). Instead, I'd look back to the definition of $H,$ and proceed directly, as follows:
Note that $g_1=f_1$ is injective by hypothesis. Supposing that $g_n$ is injective for some $n\in\Bbb N,$ we then have that $g_n=g_{n+1}\restriction_{I_n}$ is injective. Also, by definition of $H,$ we have that $g_{n+1}(n+1)=\bigl(H(g_n)\bigr)(n+1)\notin\operatorname{ran}g_n.$ Thus, since $g_{n+1}:I_{n+1}\to X,$ then $g_{n+1}$ is injective. By induction on $n,$ each $g_n$ is therefore injective.
Now, let's get back to your proof.
"We now define the required mapping $G:\Bbb N \to X$ by $G_n=g_n(n)$.
"3. $G$ is injective
"Assume the contrary that $G$ is not injective. Then there exists $n_1 < n_2$ such that $G_{n_1} = G_{n_2}$, thus $g_{n_1}(n_1) = g_{n_2}(n_2)$.
"$g_{n_1} \subseteq g_{n_1+1} \subseteq g_{n_1+2} \subseteq \cdots \subseteq g_{n_2} \implies g_{n_1} \subseteq g_{n_2}$. It follows that $g_{n_1}(n_1)=g_{n_2}(n_1) \neq g_{n_2}(n_2)$ since $g_{n_2}$ is injective. This contradicts the fact that $g_{n_1}(n_1) = g_{n_2}(n_2)$.
"Hence $G$ is injective."
You've got the idea, but you should make the induction explicit, instead of relying on "..." to fill in the blank. Instead, I'd proceed in this way:
We now define $G:\Bbb N \to X$ by $G_n=g_n(n),$ and show that it is the desired injection.
Given any $m\in\Bbb N,$ we already know that $g_m\subseteq g_{m+1}.$ Consequently, if we have $g_m\subseteq g_{m+k}$ for some $k\in\Bbb N,$ then since $g_{m+k}\subseteq g_{(m+k)+1}=g_{m+(k+1)},$ we conclude that $g_m\subseteq g_{m+(k+1)}.$ By induction on $k,$ we have $g_m\subseteq g_{m+k}$ for all $k\in\Bbb N.$ Since $m\in\Bbb N$ was arbitrary, this means that for all $m,n\in\Bbb N,$ if $m<n,$ then $g_m\subseteq g_n,$ and in particular, $g_m=g_n\restriction_{I_m}.$
Now, letting $m,n\in\Bbb N$ with $m<n,$ since $g_n$ is injective and $g_m=g_n\restriction_{I_m},$ then $G_m=g_m(m)=g_n(m)\neq g_n(n)=G_n.$ Thus, $G$ is injective, as desired. $\Box$
