Substitutions of variables are finitely axiomatizable over quantifications and permutations

This paper proves that the equational theory of the class $RA_{\alpha}^{csp}$ of representable polyadic algebras is finitely axiomatizable over its substitution-free reduct $RA_{\alpha}^{cp}$, for finite $\alpha$. That is, substitutions of variables in finite variable first-order logic can be described by finitely many axioms over the Boolean operations, existential quantifiers and permutations of variables.