How can I prove that $f:A_{n+1}\times \prod_{i\in I_n}A_i\to\prod_{i\in I_{n+1}}A_i$ is bijective? The cartesian product of a family $(A_i\mid i\in I)$ is defined as $$\prod_{i\in I}A_i=\{f:I\to\bigcup A_i\mid f(i)\in A_i\}$$
I'm trying to prove the below theorem. While I'm able to construct a desired mapping and intuitively found that it is a bijection, I'm unable to prove that this mapping is actually bijective in a formal proof. I also found that it's easier to use the definition of cartesian product as n-array, but I would like to use the definition of cartesian product as a function.

Let $I_{n+1} = \{i\in\mathbb N\mid 1\leq i\leq n+1\}$ and $(A_i\mid i\in I_{n+1})$ be a family of finite sets. Then $|A_{n+1}\times\prod_{i\in I_n}A_i|=|\prod_{i\in I_{n+1}}A_i|$ where $|X|$ is the cardinality of $X$.


First, we generate a family of indexed sets $(B_i\mid i\in I_2)$ as follows: $B_1=A_{n+1}$ and $B_2=\prod_{i\in I_n}A_i$. Then we construct a mapping $f:B_1\times B_2\to\prod_{i\in I_{n+1}}A_i$ such that $\{(0,b_1),(1,b_2)\}\mapsto \{(n+1,b_1)\cup b_2\}$ where $b_1\in B_1=A_{n+1},b_2\in B_2=\prod_{i\in I_n}A_i$.

How can I proceed to prove that $f$ is bijective?

 A: Consider
$$\begin
{array}{l|rcl}
f : & A_{n+1}\times\prod\limits_{i\in I_{n}}A_i
 & \longrightarrow & \prod\limits_{i\in I_{n+1}}A_i \\
    & \phi & \longmapsto & f(\phi) \end{array}$$
where $\phi: \{1,2\} \to A_{n+1} \bigcup \prod\limits_{i\in I_{n}}A_i$ with $\phi(1) \in A_{n+1}$ and $\phi(2) \in \prod\limits_{i\in I_{n}}A_i$.
$f(\phi)$ is defined by $$f(\phi)(i)=\begin{cases}\phi(1) & \text{ if } i=n+1\\
\phi(2)(i) & \text{ if } i \in I_n
\end {cases}$$
$f$ is surjective
For $\psi \in \prod\limits_{i\in I_{n+1}}A_i$ define $\phi \in A_{n+1}\times\prod\limits_{i\in I_{n}}A_i$ by
$$\phi(i)=\begin{cases}\psi(n+1) & \text{ if } i=1\\
\phi(2) & \text{ if } i =2
\end {cases}$$
where $\phi(2)(j)=\psi(j)$ for $j \in I_n$. $\phi(2)$ is a map belonging to $\prod\limits_{i\in I_{n}}A_i$. You’ll verify that $f(\phi)=\psi$ proving that $f$ is surjective.
$f$ is injective
This is an easy verification that $\phi_1=\phi_2$ if $f(\phi_1)=f(\phi_2)$.
A: This is a proof by mathcounterexamples.net, but I would like add full details to make sure I truly understand it. All credits go to mathcounterexamples.net.

We define mapping $f$ as follows $$\begin
{array}{l|rcl}
f : & A_{n+1}\times\prod\limits_{i\in I_{n}}A_i
 & \longrightarrow & \prod\limits_{i\in I_{n+1}}A_i \\
    & \phi & \longmapsto & f(\phi) \end{array}$$
where $\phi:\{1,2\}\to A_{n+1}\bigcup\prod\limits_{i\in I_{n}}A_i$ such that $\phi(1)\in A_{n+1}$ and $\phi(2)\in\prod\limits_{i\in I_{n}}A_i$.
We define $f(\phi)$ by ${f(\phi)|}_{I_n}=\phi(2)$ and $f(\phi)(n+1)=\phi(1)$.


*

*$f$ is surjective


For $\psi\in\prod\limits_{i\in I_{n}}A_i$, we define $\phi\in A_{n+1}\times\prod\limits_{i\in I_{n}}A_i$ by $\phi(1):=\psi(n+1)$ and $\phi(2):={\psi|}_{I_n}$. Next we prove $f(\phi)=\psi$. We have ${f(\phi)|}_{I_n}\overset{(1)}{=}\phi(2)\overset{(2)}{=}{\psi|}_{I_n}$ and $f(\phi)(n+1)\overset{(3)}{=}\phi(1)\overset{(4)}{=}\psi(n+1)$. Thus $f(\phi)=\psi$, and consequently $f$ is surjective.
(1) By the definition of $f(\phi)$
(2) By the definition of $\phi(2)$
(3) By the definition of $f(\phi)$
(4) By the definition of $\phi(1)$


*$f$ is injective


For $\phi_1,\phi_2\in A_{n+1}\times\prod\limits_{i\in I_{n}}A_i$ and $f(\phi_1)=f(\phi_2)$, then $f(\phi_1)(i)=f(\phi_2)(i)$ for all $i\in I_{n+1}$, then ${f(\phi_1)|}_{I_n}={f(\phi_2)|}_{I_n}$ and $f(\phi_1)(n+1)=f(\phi_2)(n+1)$, then $\phi_1(2)=\phi_2(2)$ and $\phi_1(1)=\phi_2(1)$. Thus $\phi_1=\phi_2$. Hence $f$ is injective.
