Unifiers modulo commutativity in terms of syntactic unifiers and $\approx_{C}$-class

Question

I am studying Term Rewriting by reading Baader's book "Term Rewriting and All That". I am in the chapter of Equational Unification, in the section of Commutative Functions. I am trying to do the following exercise:

Let $s, t \in T(\Sigma, V)$. By exercise 10.10 we know that the $\approx_{C}$-classes of these terms are finite. Let $\{s_1, \ldots, s_m \}$ be the $\approx_{C}$-class of $s$, and let $\{t_1, \ldots, t_n \}$ the $\approx_{C}$-class of $t$. Show that: $$ \mathcal{U}_{C}(\{ s \approx_{C}^{?} t \}) = \bigcup\limits_{1 \leq i \leq m \\ 1 \leq j \leq n} \mathcal{U}_{\emptyset}(\{s_i =^{?} t_j \}) $$ and that $\{ \sigma \ | \ \sigma \ \text{ is an mgu of } s_i =^{?} t_j \text{ for some } i, j, 1 \leq i \leq m, 1 \leq j \leq n \}$ is a complete set of C-unifiers of $s \approx_{C}^{?} t$.

It seems obvious, but how can I prove that: $$\mathcal{U}_{C}(\{ s \approx_{C}^{?} t \}) = \bigcup\limits_{1 \leq i \leq m \\ 1 \leq j \leq n} \mathcal{U}_{\emptyset}(\{s_i =^{?} t_j \}) ? \tag{1}$$

After I prove that, I know how to proceed: let $\delta$ be an arbitrary C-unifier of $s \approx_{C}^{?} t$. By the equation (1) above, this means that $\exists_{i, j}: \ s_i \delta = t_i \delta$. Take $\sigma$ the mgu of $s_i =^{?} t_j$ and we have that $\sigma$ is more general than $\delta$. Therefore, $\{ \sigma \ | \ \sigma \ \text{ is an mgu of } s_i =^{?} t_j \text{ for some } i, j, 1 \leq i \leq m, 1 \leq j \leq n \}$ is a complete set of C-unifiers of $s \approx_{C}^{?} t$.

How can I prove (1)? Any hint/suggestion is very much appreciated. Thanks in advance.

Answer 1

Note that for all $s, t \in T(\Sigma, V)$ we have:
$$s \approx_{C} t \iff \exists_{i, j}: s_i = t_j \tag{*}$$

Using (*) for the terms $s \sigma$ and $t \sigma$ we obtain: $$s \sigma \approx_{C} t \sigma \iff \exists_{i, j}: s_i \sigma = t_j \sigma, $$i.e, $$\mathcal{U}_{C}(\{ s \approx_{C}^{?} t \}) = \bigcup\limits_{1 \leq i \leq m \\ 1 \leq j \leq n} \mathcal{U}_{\emptyset}(\{s_i =^{?} t_j \})$$