Theorem. Given two disjoint sets $X$ and $Y$, the functions $f:X \rightarrow Z$, $g:Y \rightarrow Z$ and the inclusions $\iota_{X \rightarrow X \cup Y}: X \rightarrow X \cup Y$ and $\iota_{Y \rightarrow X \cup Y}: Y \rightarrow X \cup Y$ where $\iota_{X \rightarrow X \cup Y}(x) := x$ and $\iota_{Y \rightarrow X \cup Y}(x) := x$, respectively. Show that there is a unique function $h$, such that $h \circ \iota_{X \rightarrow X \cup Y} = f$ and $h \circ \iota_{Y \rightarrow X \cup Y} = g$.
Proof.
$$
h(x) :=
\begin{cases}
f(x) & \text{if } x \in X \\
g(x) & \text{if } x \in Y.
\end{cases}
$$
The given function $h: X \cup Y \rightarrow Z$ is unique, iff
$$ (\exists h) P(h) \wedge (\forall h') \: P(h) \wedge P(h') \rightarrow h = h', $$
where $P(h)$ is the property
$$ P(h) := (h \circ \iota_{X \rightarrow X \cup Y} = f) \wedge (h \circ \iota_{Y \rightarrow X \cup Y} = g). $$
To show that $P(h)$ holds we can pick two arbitrary elements from $X$ and $Y$, evaluate $(h \circ \iota_{X \rightarrow X \cup Y})(x) = h(x)$ or $(h \circ \iota_{Y \rightarrow X \cup Y})(x) = h(x)$, and find that $h(x) = f(x)$, if $x$ in $X$ and $h(x) = g(x)$, if $x$ in $Y$. Note that if e.g. $x \in X$, then, since $\iota_{Y \rightarrow X \cup Y}$ and $g$ are undefined on $X$, $x \in Y \rightarrow (h \circ \iota_{Y \rightarrow X \cup Y})(x) = g(x)$ is vacuously true.
Uniqueness is verified by taking the contra-positive of the 2nd clause of the definition of uniqueness:
$$ (\forall h') \: h \neq h' \rightarrow \neg P(h) \vee \neg P(h') $$
Two functions $h$ and $h'$ are equal iff for every element of their common domain the respective elements in the range are equal: $ (\forall x \in X\cup Y) \: h(x) = h'(x). $ Hence, $h$, $h'$ are not equal iff there is an element in their common domain such that the respective elements in the range are unequal: $ (\exists x \in X\cup Y) \: h(x) \neq h'(x). $
Assume an element $x \in X$. From the hypothesis and the definition of $h$ we have that $h(x) = f(x) \neq h'(x)$. It follows that $(h' \circ \iota_{X \rightarrow X \cup Y})(x) \neq f(x) \leftrightarrow \neg P(h')$. Accordingly, if $x \in Y$: $h(x) = g(x) \neq h'(x) = (h' \circ \iota_{Y \rightarrow X \cup Y})(x) \leftrightarrow \neg P(h').$
2015 FEB 12 (v1.0)