\begin{align*} \operatorname {\mathrm{Hom}}_{\mathbf{Rel}\webleft (A,X\webright )}\webleft (S\mathbin {\diamond }R,T\webright ) & \cong \int _{a\in A}\int _{x\in X}\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\webleft (S\mathbin {\diamond }R\webright )^{x}_{a},T^{x}_{a}\webright )\\ & \cong \int _{a\in A}\int _{x\in X}\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\webleft (\int ^{b\in B}S^{x}_{b}\times R^{b}_{a}\webright ),T^{x}_{a}\webright )\\ & \cong \int _{a\in A}\int _{x\in X}\int _{b\in B}\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (S^{x}_{b}\times R^{b}_{a},T^{x}_{a}\webright )\\ & \cong \int _{a\in A}\int _{x\in X}\int _{b\in B}\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (S^{x}_{b},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},T^{x}_{a}\webright )\webright )\\ & \cong \int _{b\in B}\int _{x\in X}\int _{a\in A}\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (S^{x}_{b},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},T^{x}_{a}\webright )\webright )\\ & \cong \int _{b\in B}\int _{x\in X}\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (S^{x}_{b},\int _{a\in A}\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},T^{x}_{a}\webright )\webright )\\ & \cong \operatorname {\mathrm{Hom}}_{\mathbf{Rel}\webleft (B,X\webright )}\webleft (S,\int _{a\in A}\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{-_{2}}_{a},T^{-_{1}}_{a}\webright )\webright )\end{align*}
naturally in each $S\in \mathbf{Rel}\webleft (B,X\webright )$ and each $T\in \mathbf{Rel}\webleft (A,X\webright )$, showing that
\[ \int _{a\in A}\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{-_{2}}_{a},T^{-_{1}}_{a}\webright ) \]
is right adjoint to the precomposition functor $-\mathbin {\diamond }R$, being thus the right Kan extension along $R$. Here we have used the following results, respectively (i.e. for each $\cong $ sign):
This finishes the proof.
