Finiteness of Cartesian Products, Tuple Sets, and Permutation Sets

Let $\mathbb{N}$ be the set of natural numbers with successor map $S$ as in that definition, and for $p\in\mathbb{N}$ let $[p]$ be the initial segment determined by $p$. The notions has $k$ elements and finite are those of the indicated definitions.

Let $A$ and $B$ be finite sets, let $X$ be a nonempty finite set, and let $n\in\mathbb{N}$.

Then the following hold.

1. (Cartesian products) Let $P\times Q$ denote the Cartesian product of sets $P$ and $Q$, formed with the ordered pair. For every object $a$ the map sending $b\in B$ to $(a,b)$ is a bijection from $B$ onto $\{a\}\times B$, and $A\times B$ is finite.

2. (Extending a tuple) Let $Y$ be a set. There is exactly one map

such that for every $t\in Y^{n}$ and every $x\in Y$ the tuple $q\bigl((t,x)\bigr)$ has $k$th component $t_{k}$ for every $k\in[n]$, and $S(n)$th component $x$. This map $q$ is a bijection.

3. (Tuple sets) The set $X^{n}$ of $n$-tuples in $X$ is nonempty and finite.

4. (Permutation sets) The set $S_{n}$ of permutations of $[n]$ is nonempty and finite.