# Find an elegant proof of a set-theoretic equiality about relations

I am now attempting to prove the following theorem.

I am in half-underway of the proof and it seems I can do it by myself. But the proof I am now constructing is not elegant.

Could anyone provide a nice proof?

Let $n$ is an index set (it may be a finite ordinal, for example). Let $a$ is an $n$-ary relation. Let $f$ is an $n$-indexed family of binary relations. By definition, $\operatorname{StarComp}(a;f)$ is such a $n$-ary relation that

$$L\in\operatorname{StarComp}(a;f) \Leftrightarrow \exists y\in a\forall i\in n: y_i \mathrel{f_i} L_i.$$

Theorem $\operatorname{StarComp}(\operatorname{StarComp}(a;f);g) = \operatorname{StarComp}(a;g\circ f)$ where the composition of $n$-indexed families of relations $f$ and $g$ is taken componentwise: $g\circ f = \lambda i\in n:g_i\circ f_i$.

-

Let $x R \left( f \right) y \Leftrightarrow \forall i \in n : x_i f_i y_i$.
$L \in \operatorname{GR}\operatorname{StarComp} \left( a ; f \right) \Leftrightarrow \exists y \in \operatorname{GR}a : y R \left( f \right) L$.
$L \in \operatorname{GR}\operatorname{StarComp} \left( \operatorname{StarComp} \left( a ; f \right) ; g \right) \Leftrightarrow \exists p \in \operatorname{GR}\operatorname{StarComp} \left( a ; f \right) : p R \left( g \right) L \Leftrightarrow \exists p, y \in \operatorname{GR}a : \left( y R \left( f \right) p \wedge p R \left( g \right) L \right) \Leftrightarrow \exists y \in \operatorname{GR}a : \left( y R \left( g \circ f \right) L \right) \Leftrightarrow L \in \operatorname{GR}\operatorname{StarComp} \left( a ; g\circ f \right)$.