Let $X_1, \ldots, X_{N + 1}$ each be a D11: Set such that
| (i) | $X : = \prod_{n = 1}^{N + 1} X_n$ and $Y : = (\prod_{n = 1}^N X_n) \times X_{N + 1}$ are each a D326: Cartesian product |
| (ii) | \begin{equation} f : X \to Y, \quad f(x_1, \ldots, x_{N + 1}) = ((x_1, \ldots, x_N), x_{N + 1}) \end{equation} |
| (iii) | \begin{equation} g : Y \to X, \quad g((x_1, \ldots, x_N), x_{N + 1}) = (x_1, \ldots, x_{N + 1}) \end{equation} |
Then
| (1) | $f$ is a D468: Bijective map |
| (2) | $g$ is an D216: Inverse map for $f$ |