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$.