An irreducible regular-map image contains a relative open subset

Let $K$ be an algebraically closed field, and let $X$ and $Y$ be locally closed subsets of finite products of projective spaces over $K$, with their induced Zariski topologies. Assume that $X$ is irreducible, in particular nonempty, and that $f:X\to Y$ is regular. Write $Z=\overline{f(X)}$, where the closure is taken in $Y$. Then there is a Zariski-open subset $U\subseteq Y$ such that

Thus the image contains a nonempty relatively open subset of its closure. The target need not be irreducible, and the image need not have nonempty interior in the whole target. There is no group structure or characteristic-zero assumption.

This generic-image assertion is the geometric input for Noetherian-induction proofs of constructibility. Its relative formulation allows the image to lie in a proper closed subset of the target.

Formalization Note. The proof uses finite-presentation affine coordinate maps, constructible images, and compatible closed-point charts to obtain a relative open subset of the closure of an irreducible regular-map image. The required affine chart construction is now proved, completing the original theorem. Every theorem dependency of the accepted reduction is now Proved, and this theorem has zero Open leaves. The final affine construction is proved here. The original formal statement and hypotheses are unchanged.