Lemma 86.24.9. Let $S$ be a scheme. Let $f : X \to Y$ and $Z \to Y$ be morphisms of formal algebraic spaces over $S$. If $Z$ is locally Noetherian and $f$ locally of finite type, then $Z \times _ Y X$ is locally Noetherian.

Proof. The morphism $Z \times _ Y X \to Z$ is locally of finite type by Lemma 86.24.4. Hence this follows from Lemma 86.24.8. $\square$

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).