I'm halfway through a proof and I'm kind of stuck. The exercise is:
Let $\{A_i\}_{i\in \{0, 1\}}$ be an indexed system of sets. Show that the map $$\mathbf f: \prod{\{A_i\}_{i\in \{0, 1\} }} \rightarrow A_0 \times A_1$$ given by $$f(g) =(g(0), g(1))$$ is a Bijection.
First we would like to show that $f$ is Injective: Consider two instances of input function $g$, e.g. $x$ and $y$ hence: $$f(x)=f(y)$$ $$\therefore(x(0),x(1))=(y(0),y(1))$$ $$\therefore x(0) = y(0) \land x(1)=y(1) $$ $$\mathbf {dom}(x) = \mathbf{dom}(y) = \{0, 1\}$$ $$\therefore x(i) = y(i) \forall i \in \{0, 1\}$$ $\therefore f(g)$ is Injective. Is my reasoning correct so far?
Now to showing $f$ is Surjective, we consider the the domain and codomain of the mapping, namely, the Generalised Cartesian Product of an Indexed Family of Sets: $$\prod{\{A_i\}_{i\in \{0, 1\} }}=\{\{(0,x_0 \in A_0),(1, x_1 \in A_1)\}\}$$ and the usual Cartesian Product: $$A_0 \times A_1 =(x_0 \in A_0, x_1 \in A_1)$$ respectively.
It is trivial to see that the mapping given by $f$ is Surjective, as the two ordered pair elements of $f=(g(0),g(1))$ span over all $A_0$ and $A_1$ respectively and considering that $g$ could take any arbitrary function of $\mathbf {domain}$ $\{0, 1\}$by definition of the Generalised Cartesian Product of an Indexed Family of Sets. But how do I write this formally?
Your proof of injectivity is correct, though I would add one more line concluding that $x=y$. For the proof of surjectivity, let $\langle a_0,a_1\rangle\in A_0\times A_1$ be arbitrary; then $a_0\in A_0$ and $a_1\in A_1$. Define
$$x:\{0,1\}\to A_0\cup A_1:\begin{cases} 0\mapsto a_0\\ 1\mapsto a_1\;; \end{cases}$$
then $f(x)=\langle x(0),x(1)\rangle=\langle a_0,a_1\rangle$, so $f$ is surjective.