I am using ZFC and the following definitions:
$x$ is finite iff it is in bijection with a natural number;
$x$ is infinite iff it contains an injective image of $\omega$, the set of natural numbers.
Alternatively, we also have the following definition for finite:
A set $x$ is finite if every nonempty element of the power-set of x has an inclusion minimal element.
How can this be proved making use of these definitions? Note, cardinality has not been introduced at this point.
Best Answer
Let both $X_1$ and $X_2$ be finite sets with bijective maps
$\tag 1 \sigma_1: X_1 \to n_1 $ $\tag 2 \sigma_2: X_2 \to n_2 $
to the natural numbers $n_1$ and $n_2$.
The Cartesian product of the functions $\sigma_1$ and $\sigma_2$ gives a bijection
$\tag 3 \sigma_1 \times \sigma_2: X_1 \times X_2 \to n_1 \times n_2 $
If you have defined the product of two natural numbers $n_1$ and $n_2$ then you know that $n_1 n_2$ can be put into a bijective correspondence with $n_1 \times n_2$. If you only have addition, then you have some more work to do.
The successor function $S$ can be used to define the multiplication of the natural numbers once you have addition 'bijectively nailed as a disjoint union'.
For multiplication,
$\tag 4 a × 0 = 0$
$\tag 5 a × S(b) = (a × b) + a$
and you 'nail down' the product $a \times b$ of two natural numbers to the cartesian product of two finite sets. Of course this brings us right back to Asaf's answer:
$\tag 6 A\times(B\cup\{\hat b\})=(A\times B)\cup(A\times\{\hat b\}) \; \; \hat b \notin B$