ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4887 on D326: Cartesian product
Cardinality of binary cartesian product of finite sets
Formulation 0
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}