Projection of a product-generic filter ($H=G_0\times G_1$)

For a generic filter $H$ in product forcing, let $G_0,G_1$ be its coordinate projections. They are filters in an ordered set. Given $p\in G_0$ and $q\in G_1$, choose separate pairs witnessing their membership and then a common strengthening in $H$. Upward closure puts $(p,q)$ in $H$, proving the displayed equality. Every ground-model dense factor set lifts to a dense product set, proving genericity of each projection over the ground model.