I'm reading Hodges' A Shorter Model Theory. In the section about quantifier elimination, theorem $2.7.5$ proves that some set of formulas is an elimination set of the term algebra (under a different signature). I don't understand this passage:
We claim $T_2$ implies that for any $k$ elements $(k > 0) $ there is an element distinct from all of them which satisfies $\text{Is}_F(y)$. By $(6.15)$, $T_2$ implies that if $\text{Is}_F(x_0)$ then there is a unique $x_1$ such that $\text{Is}_F(x_1)$ and $F_i(x_1) = x_0$ for all $i < n$; by $(6.18)$, $x_0 \neq x_1$. Likewise by $(6.15)$ there is $x_2$ such that $\text{Is}_F(x_2)$ and $F_i(x_2) =x_1$ for all $i < n$, and then by $(6.18)$ again, $x_2 \neq x_1$ and $x_2 \neq x_1$. Etc. etc.; this proves the claim. With $(6.16)$, the claim allows the reduction to $(7.10)$, unless the problem is to eliminate the quantifier from $\exists\ y\ \text{Is}_F(y)$. When $L_1$ has at least one constant $c$, the formula $\exists\ y\ \text{Is}_F(y)$ reduces to $\neg\bot$ by $(6.15)$; but in general it is equivalent to $\beta$.
I don't understand how the claim is proven and how it implies said reduction
Here are pictures of the relevant pages for context.
The term algebra:
Theorem 2.7.5:
