Let $X$ and $Y$ each be a D17: Finite set such that
(i) | $X \times Y$ is the D191: Binary cartesian set product of $X$ and $Y$ |
Then
\begin{equation}
|X \times Y|
= |X| |Y|
\end{equation}