Pattern closure yields an end-homogeneous sequence

If $B\subseteq \lambda$ has size $\theta$, then it has at most $\theta$ subsets of size at most $\mu$. Indeed every nonempty such subset is the range of a function $\mu \to B$: enumerate it by its cardinality, which is at most $\mu$, and fill remaining arguments with its first element. The range map is a surjection from a subcollection of ${}^{\mu }B$ onto these subsets; AC selects representatives to turn this into the cardinal bound. By F1 and F2, ${\theta }^{\mu }=(2^{\mu }{)}^{\mu }=2^{\mu \cdot \mu }=2^{\mu }=\theta$. Adding the empty subset changes no infinite bound by F2.

For such a $C$ of size at most $\mu$, increasing enumeration of finite subsets of the ordinal $\lambda$ injects $[C{]}^d$ into $C^d$. Inductively F2 gives ${\mu }^d=\mu$ for positive finite $d$, so $\mathrm{\mid }[C{]}^d\mathrm{\mid }\le \mu$. The number of functions $[C{]}^d\to r$ is at most $r^{\mu }\le (2^{\mu }{)}^{\mu }=\theta$ by F1 and step 1.1. For $C=\mathrm{\varnothing }$ or $\mathrm{\mid }C\mathrm{\mid }<d$, the domain is empty and there is exactly one pattern; this also respects the bound, including $r=1$. For $z\in \lambda \setminus C$ define its realized pattern $p_{C,z}(u)=F(u\cup \{z\})$. Its argument has size $d+1$ by $z\mathrm{\notin }C$.

Define an increasing sequence $(B_{\xi }{)}_{\xi <{\mu }^{+}}$ by F5, starting with $B_0=\theta \subseteq \lambda$. At a successor add to $B_{\xi }$, for every $C\subseteq B_{\xi }$ of size at most $\mu$ and every realized pattern $p_{C,z}$ with $z\mathrm{\notin }C$, the least ordinal $z^{\mathrm{\prime }}\in \lambda \setminus C$ realizing that pattern. This least ordinal exists by realization. At limits take unions. Steps 1.1 and 2.1 bound the number of requests by $\theta \cdot \theta =\theta$, so each successor has size $\theta$. At any limit there are at most ${\mu }^{+}\le \theta$ preceding sets of size $\theta$ by F6; AC supplies injections for the union estimate and F2 bounds the union by $\theta \cdot \theta =\theta$. Each stage contains $B_0$, giving equality. This also proves $B={\bigcup }_{\xi <{\mu }^{+}}{B}_{\xi }$ has size exactly $\theta$. All sets stay inside $\lambda$.

Every $C\subseteq B$ of size at most $\mu$ is contained in one $B_{\xi }$. For nonempty $C$, assign each member its least entry stage. There are at most $\mu$ such stages, and F3/F4 make ${\mu }^{+}$ regular, so their supremum lies below ${\mu }^{+}$. Since the sequence increases, that stage or its successor contains $C$. For empty $C$ take $\xi =0$. The representative of each realized pattern over $C$ was then added at $\xi +1<{\mu }^{+}$. Thus every realized pattern over $C$ has a representative in $B\setminus C$, with exclusion of $C$ built into the successor rule.

Since $\mathrm{\mid }B\mathrm{\mid }=\theta <\lambda$, let $a$ be the least ordinal in $\lambda \setminus B$. Recursively, at $\alpha <{\mu }^{+}$ put $C_{\alpha }=\{x_{\beta }:\beta <\alpha \}$. Its cardinality is at most $\mathrm{\mid }\alpha \mathrm{\mid }\le \mu$, and it is a subset of $B$ if the previous choices were. The pattern of $a$ over $C_{\alpha }$ is realized, since $a\mathrm{\notin }B$. By step 4.1 take $x_{\alpha }$ to be the least representative of this pattern in $B\setminus C_{\alpha }$. F5 defines the sequence from this rule, which always has an eligible value. It is injective by the exclusion of $C_{\alpha }$, and $a$ is outside its range. Equality of the chosen patterns is exactly the displayed assertion for every $d$-subset of previous nodes. At stages with fewer than $d$ previous nodes the equality has no instances but the representative still exists.