Eilenberg theorem for many-sorted formations

For every implicitly quantified type $S$ equipped with the assumption that $S$ has finitely many elements, and for every explicitly given $S$-sorted signature $\Sigma$ (assigning a type of operation symbols to each finite list of input sorts and each output sort), there exists an order isomorphism $e$ from the poset of finite-index congruence formations for $\Sigma$ to the poset of regular-language formations for $\Sigma$. Here an $S$-sorted set $X$ is an arbitrary family of types $(X_s)_{s\in S}$, $T_\Sigma(X)$ is the $S$-sorted algebra of finite $\Sigma$-terms with variables from $X$, a congruence on $T_\Sigma(X)$ is a sortwise family of equivalence relations compatible with every basic operation, and it has finite index when the disjoint union $\coprod_{s\in S}T_\Sigma(X)_s/{\Phi_s}$ is finite. A finite-index congruence formation $F$ assigns to every $X$ a set $F_X$ of congruences on $T_\Sigma(X)$ such that $F_X$ is nonempty, is closed under sortwise intersection, is upward closed under inclusion of congruence relations, is closed under pulling a selected congruence $\Theta$ on $T_\Sigma(Y)$ back along any homomorphism $f:T_\Sigma(X)\to T_\Sigma(Y)$ for which $x\mapsto[f_s(x)]_{\Theta_s}$ is surjective at every sort $s$, and contains only finite-index congruences. A language on $T_\Sigma(X)$ is a sortwise family of subsets, and a congruence $\Phi$ saturates a language $K$ when, for every sort and every $\Phi$-equivalent pair, membership in $K$ is equivalent. The syntactic congruence of $K$ relates $x,y$ of sort $s$ exactly when every congruence $\Psi$ that contains every congruence saturating $K$ also relates $x,y$; $K$ is regular exactly when this congruence has finite index. A regular-language formation $L$ assigns to every $X$ a set $L_X$ of languages on $T_\Sigma(X)$ such that every selected language is regular, every language saturated by the universal congruence is selected, whenever two languages $K,N$ are selected every language saturated by the intersection of their syntactic congruences is selected, and whenever $M\in L_Y$, $f:T_\Sigma(X)\to T_\Sigma(Y)$ has sortwise-surjective composite into the quotient by the syntactic congruence of $M$, and a language $K$ on $T_\Sigma(X)$ is saturated by the pullback of that syntactic congruence along $f$, then $K\in L_X$. Both posets are ordered by pointwise inclusion of the selected sets, so $e$ is a bijection whose forward and inverse maps preserve and reflect that order. Moreover, the two displayed conjuncts fix its action exactly: for every finite-index congruence formation $F$ and every $S$-sorted set $X$, $(eF)_X=\{K\mid \exists\Phi,\ \Phi\in F_X\ \text{and}\ \Phi\text{ saturates }K\}$; and, independently, for every regular-language formation $L$ and every $S$-sorted set $X$, $(e^{-1}L)_X=\{\Phi\mid \Phi\text{ has finite index and every language saturated by }\Phi\text{ lies in }L_X\}$. The quantifiers include the degenerate cases where $S$ is empty, where any component $X_s$ is empty or infinite, and where $\Sigma$ has no operation symbols or infinitely many of them; no nonemptiness condition on $S$ or the components of $X$, and no finiteness condition on $X$ or $\Sigma$, is assumed.