theorem for free: relation cartesian product I am digging through a paper Theorems for free and a bit confused on the source of some conjectures (page 5):

Is it an axiom or it can be implied from some other axioms?
UPD
Question is about Cartesian product definition for relations. Is it an axiom or it can be derived from relation/Cartesian production definition?
UPD2
To expand on my source of confusion.
I have tried to derive this definition, but it differs from the one given in the paper.
$\newcommand{\mc}{\mathcal}$
Then we have from the paper definitions for $\mc A$ and $\mc B$:
$$\mc A: A \iff A'$$
$$\mc B: B \iff B'$$
from Cartesian product definition
$$(X, Y) \in \mc A \times \mc B$$
$X$ and $Y$ are values from corresponding relations $\mc A$ and $\mc B$ and it is possible to expand these values:
$$X \in \mc A, X = (x, x'), \ x \in A,\ x' \in A'$$
$$Y \in \mc B, Y = (y, y'), \ y \in B,\ y' \in B'$$
and then it appears:
$$((x, x'), (y, y')) \in \mc A \times \mc B$$
Tuple type is different from the paper one.
$$((A, A'), (B, B'))\ my\ type$$
$$((A, B), (A', B'))\ paper\ type$$
What is wrong?
 A: $\newcommand{\mc}{\mathcal}$
$\mc A\times\mc B$ is not the cartesian product of $\mc A$ and $\mc B$ as sets, but it is a new definition. In fact, it is the cartesian product in the category of relations.
For example (there may be other choices of morphisms), the objects are relations, and a morphism $f : \mc A\to\mc B$ is a pair $(f_1, f_2)$ where $f_1 : A\to B$, $f_2 : A'\to B'$ such that
$$x\mc A y\implies(f_1 x)\mc B (f_2 y).$$
Then you can check that $\mc A\times \mc B$ as given above satisfies the universal property of the product where
$$\hat\pi_1 : \mc A\times\mc B\to \mc A\\\hat\pi_2 :\mc A\times\mc B\to B$$ are given by
$$(\pi_1 : A\times B\to A,\pi_1':A'\times B'\to A')\\
(\pi_2 : A\times B\to B,\pi_2':A'\times B'\to B'),$$
and given
$$f : \mc C\to \mc A\qquad g :\mc C\to\mc B,$$
we obtain
$$\langle f,g\rangle :\mc C\to\mc A\times\mc B$$
by the pair $(f_1\times g_1, f_2\times g_2)$, where notice this time the product of functions is taken in the category of sets.
A: It is a definition. The statement about a product of functions follows from the definition, since if $a,b$ are functions then $((x, y), (x', y')) \in a \times b$ iff $(x, x')\in a, (y, y')\in b$ iff $x' = ax, y' = ay$. Therefore $a\times b$ is a function, as every $(x,y)$ has a unique $(x', y')$ (this is $(ax, ay)$) such that $((x, y), (x', y'))\in a\times b$, and by definition $(a\times b)(x, y) = (ax, ay)$.
