[proofplan]
We add new constant symbols naming the tuple that should realize $\Sigma(x)$. Finite satisfiability of $\Sigma(x)$ says exactly that every finite part of the resulting expanded theory is satisfiable. Compactness then gives a model of the whole expanded theory, and the interpretations of the new constants realize every formula in $\Sigma(x)$. Finally, the full set of $L(A)$-formulas true of that tuple is a complete $n$-type extending $\Sigma(x)$.
[/proofplan]
[step:Name the desired realizing tuple by new constants]
Let $d = (d_1,\dots,d_n)$ be a tuple of new constant symbols not belonging to $L(A)$. Define the expanded language
\begin{align*}
L(A,d) := L(A) \cup \{d_1,\dots,d_n\}.
\end{align*}
For each $L(A)$-formula $\varphi(x)$ with $x = (x_1,\dots,x_n)$, let $\varphi(d)$ denote the $L(A,d)$-sentence obtained by replacing each variable $x_i$ by the constant symbol $d_i$.
Define the $L(A,d)$-theory
\begin{align*}
\Theta := T \cup \operatorname{Diag}(A) \cup \{\varphi(d) : \varphi(x) \in \Sigma(x)\}.
\end{align*}
[/step]
[step:Verify finite satisfiability of the expanded theory]
Let $\Theta_0 \subset \Theta$ be finite. Since $\Theta_0$ is finite, there are finite subsets $T_0 \subset T$, $D_0 \subset \operatorname{Diag}(A)$, and $\Sigma_0(x) \subset \Sigma(x)$ such that
\begin{align*}
\Theta_0 \subset T_0 \cup D_0 \cup \{\varphi(d) : \varphi(x) \in \Sigma_0(x)\}.
\end{align*}
By finite satisfiability over $T \cup \operatorname{Diag}(A)$, the theory
\begin{align*}
T \cup \operatorname{Diag}(A) \cup \{\exists x\, \bigwedge_{\varphi \in \Sigma_0} \varphi(x)\}
\end{align*}
has a model. Let $M$ be such a model, and choose a tuple $c = (c_1,\dots,c_n) \in M^n$ such that
\begin{align*}
M \models \varphi(c)
\end{align*}
for every $\varphi(x) \in \Sigma_0(x)$.
Expand $M$ to an $L(A,d)$-structure $M_d$ by interpreting each new constant symbol $d_i$ as $c_i$. Then
\begin{align*}
M_d \models T_0 \cup D_0 \cup \{\varphi(d) : \varphi(x) \in \Sigma_0(x)\},
\end{align*}
and hence $M_d \models \Theta_0$. Therefore every finite subset of $\Theta$ is satisfiable.
[guided]
The purpose of the new constants is to turn the problem of realizing a partial type into an ordinary satisfiability problem for sentences. A formula $\varphi(x)$ has free variables, so it is not itself a sentence of a theory. After introducing constants $d_1,\dots,d_n$, the expression $\varphi(d)$ is a sentence saying that the tuple named by $d$ satisfies $\varphi$.
We must check that the expanded theory
\begin{align*}
\Theta := T \cup \operatorname{Diag}(A) \cup \{\varphi(d) : \varphi(x) \in \Sigma(x)\}
\end{align*}
is finitely satisfiable. Let $\Theta_0 \subset \Theta$ be finite. Only finitely many formulas from $\Sigma(x)$ can occur in $\Theta_0$, so choose a finite subset $\Sigma_0(x) \subset \Sigma(x)$ such that every instance of a $\Sigma$-formula appearing in $\Theta_0$ has the form $\varphi(d)$ with $\varphi(x) \in \Sigma_0(x)$. Also choose finite subsets $T_0 \subset T$ and $D_0 \subset \operatorname{Diag}(A)$ such that
\begin{align*}
\Theta_0 \subset T_0 \cup D_0 \cup \{\varphi(d) : \varphi(x) \in \Sigma_0(x)\}.
\end{align*}
The hypothesis of finite satisfiability says that the finite collection $\Sigma_0(x)$ can be realized in some model of $T \cup \operatorname{Diag}(A)$. Thus there is an $L(A)$-structure $M$ such that
\begin{align*}
M \models T \cup \operatorname{Diag}(A)
\end{align*}
and there is a tuple $c = (c_1,\dots,c_n) \in M^n$ satisfying
\begin{align*}
M \models \varphi(c)
\end{align*}
for every $\varphi(x) \in \Sigma_0(x)$.
Now interpret the new constant symbol $d_i$ as the element $c_i$ for each $i \in \{1,\dots,n\}$. This gives an $L(A,d)$-expansion $M_d$ of $M$. Since $M$ already satisfies $T \cup \operatorname{Diag}(A)$, the expansion $M_d$ satisfies $T_0 \cup D_0$. Since each $d_i$ is interpreted as $c_i$, the truth of $\varphi(c)$ in $M$ is exactly the truth of $\varphi(d)$ in $M_d$. Hence
\begin{align*}
M_d \models T_0 \cup D_0 \cup \{\varphi(d) : \varphi(x) \in \Sigma_0(x)\}.
\end{align*}
Because $\Theta_0$ is contained in this finite satisfiable theory, $M_d \models \Theta_0$. Thus every finite subset of $\Theta$ is satisfiable.
[/guided]
[/step]
[step:Apply compactness to obtain a realization of $\Sigma(x)$]
Since every finite subset of $\Theta$ is satisfiable, the First-Order [Compactness Theorem](/theorems/2748) applies to the $L(A,d)$-theory $\Theta$ and gives an $L(A,d)$-structure $N_d$ such that
\begin{align*}
N_d \models \Theta.
\end{align*}
(citing a result not yet in the wiki: First-Order Compactness Theorem)
Let $N$ be the reduct of $N_d$ to the language $L(A)$. Since $T \cup \operatorname{Diag}(A) \subset \Theta$, we have
\begin{align*}
N \models T \cup \operatorname{Diag}(A).
\end{align*}
For each $i \in \{1,\dots,n\}$, let $b_i \in N$ be the interpretation of the constant symbol $d_i$ in $N_d$, and set
\begin{align*}
b := (b_1,\dots,b_n) \in N^n.
\end{align*}
Because $\varphi(d) \in \Theta$ for every $\varphi(x) \in \Sigma(x)$, we have
\begin{align*}
N \models \varphi(b)
\end{align*}
for every $\varphi(x) \in \Sigma(x)$.
[/step]
[step:Form the complete type realized by the tuple]
Define
\begin{align*}
p(x) := \{\psi(x) : \psi(x) \text{ is an } L(A)\text{-formula and } N \models \psi(b)\}.
\end{align*}
Then $p(x)$ contains $\Sigma(x)$, since $N \models \varphi(b)$ for every $\varphi(x) \in \Sigma(x)$.
It remains to check completeness. Let $\psi(x)$ be any $L(A)$-formula with free variables among $x_1,\dots,x_n$. By the semantics of first-order logic in the structure $N$, exactly one of the following holds:
\begin{align*}
N \models \psi(b), \qquad N \models \neg \psi(b).
\end{align*}
Therefore exactly one of $\psi(x)$ and $\neg \psi(x)$ belongs to $p(x)$. Hence $p(x)$ is a complete $n$-type over $A$, and $\Sigma(x) \subset p(x)$. This proves the claimed extension.
[/step]
