Understanding the model-theoretic proof of Hilbert's Nullstellensatz

The proof I am talking about goes like this: Given $k$ algebraically closed and $(f_1,..,f_k)=I\neq (1)$ an ideal in $A=k[x_1,..,x_n]$, let $m$ be a maximal ideal with $I\subseteq m$ and observe that $k$ embeds into the algebraic closure $k'$ of $A/m$ , and that $f_1,..,f_k$ have the common zero $(\overline x_1,..,\overline x_n)$ in the extension field. Now use model-completeness of the theory $\Phi$ of $k$, which is the same as the theory of $k'$, and conclude that $\Phi \models \exists y_1,..,y_n f_1(y_1,..,y_n)\land ..\land f_k(y_1,..,y_n)$, because this holds in $k'$, so it must hold in $k$ also.

The proof is described for example here on page 89 and here on page 8 and 9.

My problem is: $\exists y_1,..,y_n f_1(y_1,..,y_n)\land ..\land f_k(y_1,..,y_n)$ is not immediately a formula over the laguage of fields, since it contains the symbols/functions $f_1,..,f_k$ which are not part of that language. I can see how to restate this formula using only symbols of the language of fields in the case that $f_1,..,f_k$ have integral coefficients, but not in the general case. (e.g. for $k=\mathbb{C}$ there are uncountably many possiblities for coefficients)

-

But polynomials are formulas in the language of fields.

I mean what is an atomic formula in the language of fields? It has no relations except equality. So we have to claim that two terms are equal, but instead we can claim that the difference is zero. So we can always assume that this is a sum of two terms being equal zero.

What is a term? We have finitely many free variables, $x_1,\ldots,x_n$, and multiplication either by one another or by parameters (that is scalars) and finally... addition.

So we have finitely many variables and we are allowed to multiply them by one another, and by scalars from the field, and then we add everything up and we claim it is equal to zero. What do we end up with? A polynomial in $k[x_1,\ldots,x_n]$!

So atomic formulas are just polynomials. From there the rest follows.

-
But what about the coefficients? I mean, how can you e.g. state that something is a zero of $\pi X +1\in \mathbb{C}[X]$ – user35359 Dec 22 '12 at 0:01
@user35359: You allow parameters. What are parameters if not elements from the model, i.e. scalars? – Asaf Karagila Dec 22 '12 at 0:04
@user35359: Note that $\pi X+1$ is a term. When you assign $X$ a value then it becomes just a complex number. The formula stating that this term is equal to $0$ is just $\pi X+1=0$, and it is true if and only if you assign $X$ a particular value, in this case $-\frac1\pi$. – Asaf Karagila Dec 22 '12 at 0:07
Ah, I get it now. The definition of elementary substructure allows using free variables in a formula which is supposed to be equivalent in both structures as long as they are interpreted as some fixed elements of the substructure. Somehow I missed that, I was thinking only of sentences. – user35359 Dec 22 '12 at 0:09
@user35359: this is precisely the part which uses model completeness. – tomasz Dec 22 '12 at 11:09