$\newcommand{\Ult}{\operatorname{Ult}}$ Lemma 19.5 of Jech's Set Theory, also called the Factor Lemma, states the following:
Let us assume that $\Ult^{(\alpha)}$ is well-founded. Then for each $\beta$, the iterated ultrapower $\Ult^{(\beta)}_{U^{(\alpha)}}(\Ult^{(\alpha)})$ taken in $\Ult^{(\alpha)}$ is isomorphic to the iterated ultrapower $\Ult^{(\alpha + \beta)}$.
Moreover, there is for each $\beta$ and isomorphism $e_\beta^{(\alpha)}$ such that for all $\xi$ and $\eta$, $i_{\xi,\eta}$ denotes the elementary embedding of $\Ult_{U^{(\alpha)}}^{(\xi)}(\Ult^{(\alpha)})$ into $\Ult^{(\eta)}_{U^{(\alpha)}}(\Ult^{(\alpha)})$, then the following diagram commutes:
The proof that Jech provided is as follows, slightly reworded for my own readability:
We induct on $\beta$. If $\beta = 0$, then the zeroth iterated ultrapower in $\Ult^{(\alpha)}$ is $\Ult^{(\alpha)}$, so we can simply let $e_0^{(\alpha)}$ be the identity mapping.
Suppose $e_\beta^{(\alpha)} : \Ult^{(\beta)}_{U^{(\alpha)}} \to \Ult^{(\alpha+\beta)}_U$ is an isomorphism. Now we have that $\Ult^{(\beta+1)}_{U^{(\alpha)}}$ and $\Ult^{(\alpha+\beta+1)}_U$ are ultrapowers of $\Ult^{(\beta)}_{U^{(\alpha)}}$ and $\Ult^{(\alpha+\beta)}_U$, respectively, mod $i_{0,\beta}^{(\alpha)}(U^{(\alpha)})$ and mod $i_{0,\alpha+\beta}(U)$, respectively. Since $i_{0,\alpha+\beta}(U) = e_\beta^{(\alpha)}(i_{0,\beta}^{(\alpha)}(U^{(\alpha)}))$(by induction), the isomorphism $e_\beta^{(\alpha)}$ induces an isomorphism $e_{\beta+1}^{(\alpha)}$ between $\Ult^{(\beta+1)}_{U^{(\alpha)}}$ and $\Ult^{(\alpha+\beta+1)}_U$.
If $\lambda$ is a limit ordinal, then $\Ult^{(\lambda)}_{U^{(\alpha)}}$ and $\Ult^{(\alpha+\lambda)}_U$ are (in $\Ult^{(\alpha)}$) the direct limits of $\{(\Ult^{(\beta)}_{U^{(\alpha)}},i_{\beta,\gamma}^{(\alpha)}) : \beta,\gamma < \lambda\}$ and $\{(\Ult^{(\alpha+\beta)}_{U},i_{\alpha+\beta,\alpha+\gamma} : \beta,\gamma < \lambda\}$, respectively. Similar to the argument for successor case, the isomorphisms $e_\beta^{(\alpha)}$, $\beta < \lambda$, will induce an isomorphism $e_\lambda^{(\alpha)}$ between $\Ult^{(\lambda)}_{U^{(\alpha)}}$ and $\Ult^{(\alpha+\lambda)}_U$.
My question is very simple. Where is well-foundedness used in the proof of the Factor Lemma?
Any help is appreciated.
