For any sets $$X$$ and $$Y$$, let $$Y^X$$ denote the set of all functions with domain $$X$$ and image contained in $$Y$$.1

Let sets $$A$$ and $$B$$ be given.

For sets $$Q$$ and functions $$q_A$$ and $$q_B$$, we define the predicate

$$\mathtt{Compatible}_{A,B}(Q,q_A,q_B)$$: $$q_A \in A^Q$$ and $$q_B \in B^Q$$.

If $$\mathtt{Compatible}_{A,B}(P,p_A,p_B)$$ is true, define the predicate

$$\mathtt{Prod}_{A,B}(P,p_A,p_B)$$: If $$\mathtt{Compatible}_{A,B}(Q,q_A,q_B)$$ is true, then there exists a unique function $$f \in P^Q$$ such that $$p_A \circ f = q_A$$ and $$p_B \circ f = q_B$$.

# Theorem

If $$\mathtt{Prod}_{A,B}(P,p_A,p_B)$$ is true and $$\mathtt{Prod}_{A,B}(Q,q_A,q_B)$$ is true, then there is a bijection $$P \to Q$$.

## Proof

Because $$\mathtt{Prod}_{A,B}(P,p_A,p_B)$$ is true and $$\mathtt{Compatible}_{A,B}(Q,q_A,q_B)$$ is true, there is a unique function $$f \in P^Q$$ such that $$$$p_A \circ f = q_A \label{qA}$$$$ and $$$$\quad p_B \circ f = q_B. \label{qB}$$$$

Because $$\mathtt{Prod}_{A,B}(Q,q_A,q_B)$$ is true and $$\mathtt{Compatible}_{A,B}(P,p_A,p_B)$$ is true, there is a unique function $$g \in Q^P$$ such that $$$$q_A \circ g = p_A \label{pA}$$$$ and $$$$\quad q_B \circ g = p_B. \label{pB}$$$$

From $$f \in P^Q$$ and $$g \in Q^P$$, it follows that $$f \circ g \in P^P$$. Define $$\phi = f \circ g, \qquad \phi \in P^P.$$

From $$\phi \in P^P$$ and $$p_A \in A^P$$, it follows that $$p_A \circ \phi \in A^P$$. From $$\phi \in P^P$$ and $$p_B \in B^P$$, it follows that $$p_B \circ \phi \in B^P$$. Therefore, $$\mathtt{Compatible}_{A,B}(P,p_A \circ \phi,p_B \circ \phi)$$ is true.

Because $$\mathtt{Prod}_{A,B}(P,p_A,p_B)$$ is true and $$\mathtt{Compatible}_{A,B}(P,p_A \circ \phi,p_B \circ \phi)$$ is true, there is a unique function $$h \in P^P$$ such that $$$$p_A \circ h = p_A \circ \phi \label{pAphi}$$$$ and $$$$p_B \circ h = p_B \circ \phi. \label{pBphi}$$$$

But \begin{align*} p_A \circ \phi&= p_A \circ (f \circ g)\\ &=(p_A \circ f) \circ g \quad \textrm{by associativity}\\ &=q_A \circ g \quad \textrm{by \eqref{qA}}\\ &=p_A \quad \textrm{by \eqref{pA}} \end{align*} and \begin{align*} p_B \circ \phi&=p_B \circ (f \circ g)\\ &=(p_B \circ f) \circ g \quad \textrm{by associativity}\\ &=q_B \circ g \quad \textrm{by \eqref{qB}}\\ &=p_B \quad \textrm{by \eqref{pB}}. \end{align*}

Thus $$\eqref{pAphi}$$ is equivalent with $$p_A \circ h = p_A$$ and $$\eqref{pBphi}$$ is equivalent with $$p_B \circ h = p_B.$$

Thus, $$\textrm{id}_P \in P^P$$ satisfies $$\eqref{pAphi}$$ and $$\eqref{pBphi}$$. Because $$h$$ is the unique element of $$P^P$$ satsifying $$\eqref{pAphi}$$ and $$\eqref{pBphi}$$, it follows that $$h=\textrm{id}_P.$$

From $$g \in Q^P$$ and $$f \in P^Q$$, it follows that $$g \circ f \in Q^Q$$. Define $$\psi = g \circ f, \qquad \psi \in Q^Q.$$

From $$\psi \in Q^Q$$ and $$q_A \in A^Q$$, it follows that $$q_A \circ \psi \in A^Q$$. From $$\psi \in Q^Q$$ and $$q_B \in B^Q$$, it follows that $$q_B \circ \psi \in B^Q$$. Therefore, $$\mathtt{Compatible}_{A,B}(Q,q_A \circ \psi,q_B \circ \psi)$$ is true.

Because $$\mathtt{Prod}_{A,B}(Q,q_A,q_B)$$ is true and $$\mathtt{Compatible}_{A,B}(Q,q_A \circ \psi,q_B \circ \psi)$$ is true, there is a unique function $$k \in Q^Q$$ such that $$$$q_A \circ k = q_A \circ \psi \label{qApsi}$$$$ and $$$$q_B \circ k = q_B \circ \psi. \label{qBpsi}$$$$

But \begin{align*} q_A \circ \psi&=q_A \circ (g \circ f)\\ &=(q_A \circ g) \circ f \quad \textrm{by associativity}\\ &=p_A \circ f \quad \textrm{by \eqref{pA}}\\ &=q_A \quad \textrm{by \eqref{qA}} \end{align*} and \begin{align*} q_B \circ \psi&=q_B \circ (g \circ f)\\ &=(q_B \circ g) \circ f \quad \textrm{by associativity}\\ &=p_B \circ f \quad \textrm{by \eqref{pB}}\\ &=q_B \quad \textrm{by \eqref{qB}}. \end{align*}

Thus $$\eqref{qApsi}$$ is equivalent with $$q_A \circ k = q_A$$ and $$\eqref{qBpsi}$$ is equivalent with $$q_B \circ k = q_B.$$

Thus, $$\textrm{id}_Q \in Q^Q$$ satisfies $$\eqref{qApsi}$$ and $$\eqref{qBpsi}$$. Because $$k$$ is the unique element of $$Q^Q$$ satsifying $$\eqref{qApsi}$$ and $$\eqref{qBpsi}$$, it follows that $$k=\textrm{id}_Q.$$

References2 3

1. Indeed, this makes sense when one or both of $$X$$ or $$Y$$ is the empty set.