¹That is, a sort-preserving mapping from Vars(t₁,t′₁,…,t_n,t′_n), the set of all variables appearing in the terms t_i or t′_i, to T_Σ(X).