Theorem. Given two sets $X$ and $Y$, the functions $f:Z \rightarrow X$, $g:Z \rightarrow Y$ and the coordinate functions $\pi_{X \times Y \rightarrow X}: X \times Y \rightarrow X$ and $\pi_{X \times Y \rightarrow Y}: X \times Y \rightarrow Y$ where $\pi_{X \times Y \rightarrow X}(x, y) := x$ and $\pi_{X \times Y \rightarrow Y}(x, y) := y$, respectively. Show that there is a unique function $h:Z \rightarrow X \times Y$, such that $\pi_{X \times Y \rightarrow X} \circ h = f$ and $\pi_{X \times Y \rightarrow Y} \circ h = g$.

Proof.

The function $h$ exists since $$ h = (f, g) =: f \oplus g $$ satisfies the property $$ P(h) = (\pi_{X \times Y \rightarrow X} \circ h = f) \wedge (\pi_{X \times Y \rightarrow Y} \circ h = g).$$ Uniqueness of $h$ is given iff $$ (\forall h') \: P(h) \wedge P(h') \rightarrow h = h'. $$ Or, equivalently, $$ (\forall h') \: h \neq h' \rightarrow \neg P(h) \vee \neg P(h') . $$ Two functions $h$, $h'$ are not equal iff there is an element $z$ in the common domain such that the respective elements in the range are not equal: $$ h \neq h' \leftrightarrow (\exists z \in Z) \: h(z) \neq h'(z) \leftrightarrow (h_1(z) \neq h_1'(z) \vee h_2(z) \neq h_2'(z)). $$ Given $h_1(z) \neq h_1'(z)$ we have that $$ (\pi_{X \times Y \rightarrow X} \circ h')(z) \neq f(z) \rightarrow \neg P(h'). $$ Accordingly, if $h_2(z) \neq h_2'(z)$ $$ (\pi_{X \times Y \rightarrow Y} \circ h')(z) \neq g(z) \rightarrow \neg P(h'). $$ $\Box$

• Back to menu