Bounding finite-image sequences of length $\omega^k$

Given a well-quasi-order $X$ and an ordinal $\alpha$, the set $s^F_\alpha(X)$ of transfinite sequences on $X$ with length less than $\alpha$ and with finite image is also a well-quasi-order, as proven by Nash-Williams. Before Nash-Williams proved it for general $\alpha$, however, it was proven for $\alpha<\omega^\omega$ by Erd\H{o}s and Rado. In this paper, we revisit Erd\H{o}s and Rado's proof and improve upon it, using it to obtain upper bounds on the maximum linearization of $s^F_{\omega^k}(X)$ in terms of $k$ and $o(X)$, where $o(X)$ denotes the maximum linearization of $X$. We show that, for fixed $k$, $o(s^F_{\omega^k}(X))$ is bounded above by a function which can roughly be described as $(k+1)$-times exponential in $o(X)$. We also show that, for $k\le 2$, this bound is not far from tight.