I'm trying to solve the following exercise ("Mathematical Analysis I" by Zorich, Ch. 1, Ex. 1):
The composition $R_2 \circ R_1$ of the relations $R_1$ and $R_2$ is defined as follows: if $R_1 \subset X \times Y$ and $R_2 \subset Y \times Z$, then $R=R_2\circ R_1 \subset X\times Z$, and
$$xRz := \exists y ~\big((y\in Y) \land (xR_1y)\land(yR_2 z)\big)$$
Let $\Delta_X$ be the diagonal of $X^2$ and $\Delta_Y$ the diagonal of $Y^2$. Show that if the relations $R_1 \subset X\times Y$ and $R_2 \subset Y\times X$ are such that $(R_2\circ R_1=\Delta_X)\land(R_1\circ R_2=\Delta_Y)$, then both relations are functional and define mutually inverse mappings of $X$ and $Y$.
For reference, here's the definition of a functional relation:
If $X$ and $Y$ are two sets, not necessarily distinct, a relation $R \subset X\times Y$ between elements $x$ of $X$ and $y$ of $Y$ is a functional relation on $X$ if for every $x\in X$, there exists a unique element $y\in Y$ in the given relation to $x$, that is, such that $xRy$ holds.
Attempt: For the first part, I'm just trying to show that $R_1$ is a functional relation (by symmetry, $R_2$ will be as well). Let any $x \in X$ be given. The fact that $R_2\circ R_1 = \Delta_X$ implies that $x(R_2\circ R_1)x$, or by definition, that $\exists y~\big((y\in Y)\land (xR_1 y)\land(yR_2 x)\big) \implies \exists y~(xR_1 y)$.
(Uniqueness) Assume that $xR_1 y'$ for some $y'\in Y$ and $y'\neq y$. By the same argument above, $\exists x'~\big((y'R_2 x')\land(x'R_1 y')\big)$. If $x'\neq x$, we have
$$\exists y'~\big((y'\in Y)\land(xR_1 y')\land(y'R_2 x')\big) =: x\Delta_X x'$$
which is a contradiction to the definition of $\Delta_X$. If $x=x'$, then $xR_1 y'$, i.e.
$$\exists x~\big((x\in X)\land(yR_2 x)\land(xR_1 y')\big) =: y\Delta_Y y'$$
again a contradiction.
Let $x \in X$ such that $xR_1 y'$. For each $x\in X$, we showed in the first part that there's a $y \in Y$ such that $\big((xR_1 y)\land(yR_2 x)\big)$. By uniqueness, $y'=y \implies y'R_2 x$. The reverse implication is proved similarly to show that $R_1$ and $R_2$ are inverse relations.
I'm not sure about the proof for uniqueness and inverse relation. Would be nice if it could be verified.