Lexicographic order on $\alpha^\beta$ is well-ordered Suppose that $\alpha$ and $\beta$ are ordinals, and define the following order on $\alpha^\beta$, the set of all functions $\beta\to\alpha$ with finite support:
$$f\,R\,g\iff\exists x\in\beta\,(f(x)<g(x)\land\forall y\in\beta\,(x<y\to f(y)=g(y)))$$
I wish to prove that $R$ is a well order of $\alpha^\beta$. I have already shown that $R$ is a total order on $\alpha^\beta$, so it remains to prove that if $S$ is a nonempty subset of $\alpha^\beta$ then it contains an $R$-minimal element, but I'm at a loss as for how to select this element and the Wikipedia section on this is rather terse with respect to actual proofs.

Here is an alternative solution, which additionally establishes that the order type of $R$ is $\alpha^\beta$, by constructing an explicit order isomorphism from the set $A=\{f:\beta\to\alpha:f\mbox{ has finite support}\}$ to the ordinal $\alpha^\beta$ (defined recursively via $\alpha^{\beta+1}=\alpha^\beta\alpha$, $\alpha^\delta=\bigcup_{\beta<\delta}\alpha^\beta$ for limit $\delta$).
Given $f:\beta\to\alpha$, let $(a_i)_{1\le i\le n}$ enumerate the indexes $\delta$ at which $f(\delta)\ne0$ in descending order, and define $$F(f)=\sum_{i=1}^n\alpha^{a_i}f(a_i).$$
The bijectivity (and with a more careful analysis, strict monotonicity) of $F$ follows from the basis representation theorem, an extension of the Cantor Normal Form theorem.
