Let $\varphi$ be an mso formula over $A$ whose free variables are among the first-order variables $x_1, \ldots, x_k$ and the set variables $X_1, \ldots, X_\ell$. Then the language over $A \times 2^{k+\ell}$ of the annotated strings $w \otimes \{x_1\} \otimes \cdots \otimes \{x_k\} \otimes X_1 \otimes \cdots \otimes X_\ell$ such that $w \models \varphi(x_1, \ldots, x_k, X_1, \ldots, X_\ell)$ is regular (Lemma C.4.2 of Transducers). The proof is an induction on the formula, with a nondeterministic automaton guessing the value of a quantified variable.