Let $X$ and $Y$ each be a D16: Countable set such that

(i)	$X \times Y$ is the D191: Binary cartesian set product of $X$ with $Y$

Due to results

(i)	R507: Empty set is countable
(ii)	R10: Binary cartesian product with empty set is empty

we may assume that $X \times Y$ as well as $X$ and $Y$ are each nonempty.

Since $X$ and $Y$ are countable, then there exists surjections $f : \mathbb{N} \to X$ and $g : \mathbb{N} \to Y$. Define the map \begin{equation} h : \mathbb{N} \times \mathbb{N} \to X \times Y, \quad h(n, m) : = (f(n), g(m)) \end{equation} The goal is to show that $h$ is a surjection. To this end, fix $(x, y) \in X \times Y$. Since $f$ and $g$ are surjections, then there exists $n, m \in \mathbb{N}$ such that $f(x) = n$ and $f(y) = m$. Result R3346: Characterisation of equality of ordered pairs implies that $(n, m) = (f(x), f(y)) = h(x, y)$ and hence $h$ is a surjection.

Result R511: Natural number plane is countable shows that there exists a surjection $s : \mathbb{N} \to \mathbb{N} \times \mathbb{N}$. We can now form the composite map \begin{equation} h \circ s : \mathbb{N} \to X \times Y, \quad (h \circ s)(n) = (f(n), g(m)) \end{equation} whence result R315: Composition of surjections is surjection guarantees that $h \circ s$ is a surjection. This finishes the proof. $\square$