[proofplan] We translate the semialgebraic description of $A$ into a quantifier-free formula in the language of ordered rings with parameters from $F$. The image under projection is then described exactly by existentially quantifying the eliminated coordinate. Tarski-Seidenberg quantifier elimination for real closed fields removes this existential quantifier, producing a quantifier-free formula in the remaining variables. That quantifier-free formula defines a semialgebraic subset of $F^n$, which is precisely $\pi(A)$. [/proofplan]

[step:Represent $A$ by a quantifier-free formula with parameters from $F$] Because $A \subset F^{n+1}$ is semialgebraic over $F$, there exists a quantifier-free formula $\theta(x_1,\dots,x_n,y)$ in the language of ordered rings, with parameters from $F$, such that for every $(a_1,\dots,a_n,b) \in F^{n+1}$, \begin{align*} (a_1,\dots,a_n,b) \in A \iff F \models \theta(a_1,\dots,a_n,b). \end{align*} Here $F \models \theta(a_1,\dots,a_n,b)$ means that the formula $\theta$ is true in the ordered field $F$ after substituting $a_i$ for $x_i$ and $b$ for $y$. [/step]

[step:Express the projection by existential quantification] Define the formula $\varphi(x_1,\dots,x_n)$ by \begin{align*} \varphi(x_1,\dots,x_n) \equiv \exists y\, \theta(x_1,\dots,x_n,y). \end{align*} For every $a=(a_1,\dots,a_n) \in F^n$, we have \begin{align*} a \in \pi(A) &\iff \text{there exists } b \in F \text{ such that } (a_1,\dots,a_n,b) \in A \\ &\iff \text{there exists } b \in F \text{ such that } F \models \theta(a_1,\dots,a_n,b) \\ &\iff F \models \exists y\,\theta(a_1,\dots,a_n,y) \\ &\iff F \models \varphi(a_1,\dots,a_n). \end{align*} Thus $\pi(A)$ is the subset of $F^n$ defined by the first-order formula $\varphi$. [/step]

[step:Eliminate the existential quantifier over the real closed field $F$] By Tarski-Seidenberg quantifier elimination for real closed fields (citing a result not yet in the wiki: [Tarski-Seidenberg Quantifier Elimination Theorem](/theorems/4315) for real closed fields), every first-order formula in the language of ordered rings with parameters from $F$ is equivalent over the real closed field $F$ to a quantifier-free formula with the same free variables and the same parameters. Applying this result to $\varphi(x_1,\dots,x_n)$, there exists a quantifier-free formula $\eta(x_1,\dots,x_n)$ in the language of ordered rings, with parameters from $F$, such that for every $a=(a_1,\dots,a_n) \in F^n$, \begin{align*} F \models \varphi(a_1,\dots,a_n) \iff F \models \eta(a_1,\dots,a_n). \end{align*} Combining this equivalence with the previous step gives \begin{align*} a \in \pi(A) \iff F \models \eta(a_1,\dots,a_n) \end{align*} for every $a=(a_1,\dots,a_n) \in F^n$. [/step]

[step:Conclude that the quantifier-free definition is semialgebraic] A quantifier-free formula in the language of ordered rings with parameters from $F$ is a finite Boolean combination of polynomial equalities and polynomial inequalities with coefficients in $F$. Therefore the subset of $F^n$ defined by $\eta(x_1,\dots,x_n)$ is semialgebraic over $F$. Since this subset is exactly $\pi(A)$ by the equivalence established above, $\pi(A)$ is semialgebraic over $F$. This proves the theorem. [/step]