Products of nonempty projective varieties exist as projective varieties

Inside the rank-one locus, the opens $z_{i_0{j}_0}\mathrm{\ne }0$ cover. On each such open, the regular inverse coordinates from the Segre theorem identify the desired subset with the product of the corresponding affine pieces of $X$ and $Y$, hence with a closed subset of that chart. Closedness is local on this finite open cover, so the restricted Segre image is a closed projective algebraic set.

The inverse coordinate recovery in the Segre theorem identifies this set with pairs $(x,y)\in X{\times }_{\mathrm{s}\mathrm{e}\mathrm{t}}Y$; the displayed regular ratios show on every chart that both coordinate projections are morphisms. Thus the Segre point map and its inverse are morphisms for this constructed structure.

A pair of morphisms into $X,Y$ has on each inverse-image product chart the Segre coordinate formula $[f_i{g}_j]$. These local formulas are regular and agree on overlaps, so they give a morphism into the closed model. The coordinate projections recover the given maps, and the point-pair identification makes the factorization unique. Hence this model has the product universal property.

The nonempty standard affine opens of $X$ and $Y$ are affine varieties. Their pairwise products are affine varieties by the affine-product theorem, and they cover the Segre model. Any two such product opens meet: their factor opens meet by irreducibility of $X$ and $Y$, and choosing one point from each of those two nonempty intersections gives a point of both product opens. Thus the covering affine opens all meet, so their union is irreducible. The model is therefore a nonempty projective variety.