Internally increasing hulls dominate countable tail bounds

The top function $t$ belongs to $Y_B$: by F3 and A1, $\mathrm{cf}(t(n))={\mathrm{\aleph }}_n>\omega$ for every $n\in B$, so F2 applies. Its coordinates with cofinality at most $\kappa$ are exactly those with $n\le k$, since the finite alephs strictly increase. Apply F4 at $t$, with cutoff ${\mathrm{\aleph }}_k$ and the parameters in $A$. It supplies $M$ as stated; its hull point is exactly the displayed $x$. In particular every tail coordinate has cofinality $\kappa$ and lies strictly below its top.

At an initial coordinate $n\le k$ the value $x(n)={\mathrm{\aleph }}_n$ has uncountable cofinality at most ${\mathrm{\aleph }}_k$ by F3. On the tail the same upper cofinality bound follows from step 1.1. Therefore all coordinate cofinalities lie strictly between $\omega$ and ${\mathrm{\aleph }}_{k+1}$, and F1 gives $x\in X_R(B)$. Its initial values give $x\in F_k$ by the displayed definition. This includes the possibility that $B$ has no coordinates at most $k$. The strict interpolation assertion follows from F4, applied to this very hull point: for each $b\in P_B$ with $b<x$, it returns $z\in M\cap P_B$ with $b<z<x$.

Fix $u\in M\cap P_B$ and $n>k$ in $B$ with $u(n)<{\mathrm{\aleph }}_n$. Since $n<\omega <\kappa$ and $\kappa \subseteq M$, $n\in M$. Elementarity puts the unique value $u(n)$ and its ordinal successor in $M$. These operations agree with the actual operations in $V_{\theta }$: their defining formulas are membership in the function and $s=u(n)\cup \{u(n)\}$, and all the function entries and these finite-rank codes are in the sufficiently large rank level. The infinite cardinal ${\mathrm{\aleph }}_n$ is a limit ordinal, so $u(n)+1<{\mathrm{\aleph }}_n$. Consequently $u(n)+1\in M\cap {\mathrm{\aleph }}_n$ and $u(n)<u(n)+1\le \sup (M\cap {\mathrm{\aleph }}_n)=x(n)$. Transitivity F5 ensures that the bounded membership formulas just used range over the actual function entries and ordinal members. This uses only the strict coordinate bound on $u(n)$, and applies also to zero and successor values. QED.