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

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.

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 \})$$