The Clowder Project

1. We have $\webleft (a,x\webright )\sim _{\webleft (R\times S\webright )^{\dagger }}\webleft (b,y\webright )$ iff :
   • We have $\webleft (b,y\webright )\sim _{R\times S}\webleft (a,x\webright )$, i.e. iff :
     • We have $b\sim _{R}a$;
     • We have $y\sim _{S}x$;
2. We have $\webleft (a,x\webright )\sim _{R^{\dagger }\times S^{\dagger }}\webleft (b,y\webright )$ iff :
   • We have $a\sim _{R^{\dagger }}b$ and $x\sim _{S^{\dagger }}y$, i.e. iff :
     • We have $b\sim _{R}a$;
     • We have $y\sim _{S}x$.

These two conditions agree, and thus the two resulting relations on $A\times X$ are equal.

1. We have $\webleft (a,x\webright )\sim _{\webleft (S_{1}\mathbin {\diamond }R_{1}\webright )\times \webleft (S_{2}\mathbin {\diamond }R_{2}\webright )}\webleft (c,z\webright )$ iff :
   1. We have $a\sim _{S_{1}\mathbin {\diamond }R_{1}}c$ and $x\sim _{S_{2}\mathbin {\diamond }R_{2}}z$, i.e. iff :
      1. There exists some $b\in B$ such that $a\sim _{R_{1}}b$ and $b\sim _{S_{1}}c$;
      2. There exists some $y\in Y$ such that $x\sim _{R_{2}}y$ and $y\sim _{S_{2}}z$;
2. We have $\webleft (a,x\webright )\sim _{\webleft (S_{1}\times S_{2}\webright )\mathbin {\diamond }\webleft (R_{1}\times R_{2}\webright )}\webleft (c,z\webright )$ iff :
   1. There exists some $\webleft (b,y\webright )\in B\times Y$ such that $\webleft (a,x\webright )\sim _{R_{1}\times R_{2}}\webleft (b,y\webright )$ and $\webleft (b,y\webright )\sim _{S_{1}\times S_{2}}\webleft (c,z\webright )$, i.e. such that:
      1. We have $a\sim _{R_{1}}b$ and $x\sim _{R_{2}}y$;
      2. We have $b\sim _{S_{1}}c$ and $y\sim _{S_{2}}z$.

These two conditions agree, and thus the two resulting relations from $A\times X$ to $C\times Z$ are equal.