Let $f$, $g$, $a$, $b$ are binary relations on some set.
I want an elegant proof that $(a\circ f^{-1})\cap(g^{-1}\circ b) \ne \varnothing \Leftrightarrow (\operatorname{dom}a\times\operatorname{dom}b)\cap f\ne\varnothing \wedge (\operatorname{im}a\times\operatorname{im}b)\cap g\ne\varnothing$.
I have a solution myself (I have reduced it to the special case when $\operatorname{card}a=\operatorname{card}b=1$.) But I want a more direct and more elegant proof.
Let $x,y,z,w,p,q,r,s$ be distinct elements of a set $S$, and define
$$A=\bigl\{(z,r),(p,y)\bigr\},\ B=\bigl\{(x,s),(q,w)\bigr\},\ F=\bigl\{(z,x)\bigr\},\ G=\bigl\{(y,w)\bigr\}\,.$$
Then $\bigl[\mathrm{Dom}(A)\times\mathrm{Dom}(B)\bigr]\cap F=F\ne\emptyset, \bigl[\mathrm{Im}(A)\times\mathrm{Im}(B)\bigr]\cap G=G\ne\emptyset$, and yet $A\circ F^{-1}=\bigl\{(x,r)\bigr\}$ and $G^{-1}\circ B=\bigl\{(q,y)\bigr\}$, so $\bigr[A\circ F^{-1}\bigl]\cap\bigl[G^{-1}\circ B\bigr]=\emptyset$. I constructed this example based on my previous attempt to proving the equivalence. Thus, the implication
$$\Bigl[\bigl[\mathrm{Dom}(A)\times\mathrm{Dom}(B)\bigr]\cap F\ne\emptyset\ \wedge\ \bigl[\mathrm{Im}(A)\times\mathrm{Im}(B)\bigr]\cap G\ne\emptyset\Bigr]\Rightarrow\bigr[A\circ F^{-1}\bigl]\cap\bigl[G^{-1}\circ B\bigr]=\emptyset$$
is false, though the other implication is always true (as I proved in my previous comment/answer).