[proofplan]
We use the [Definability of Types in Stable Theories](/page/Definability%20of%20Types%20in%20Stable%20Theories) to choose a coherent $M$-[definitional scheme](/page/Definitional%20Scheme) for the [complete type](/page/Complete%20Type) $p$. The scheme is chosen compatibly with Boolean operations, so it decides every instance $\varphi(x;c)$ with $c$ from the monster model, and these decisions define a [global type](/page/Global%20Type) $\tilde q$. Coherence of the scheme gives completeness and finite consistency, while the fact that the defining predicates have parameters from $M$ gives $M$-[invariance](/page/Invariant%20Type). Finally, restricting $\tilde q$ to the parameter set $B = M \cup A$ gives the desired extension of $p$ over $B$.
[/proofplan]
[step:Choose a coherent definitional scheme for the type over $M$]
By the [Definability of Types in Stable Theories](/page/Definability%20of%20Types%20in%20Stable%20Theories), every [complete type](/page/Complete%20Type) over a model of a [stable theory](/page/Stable%20Theory) has a Boolean-compatible [definitional scheme](/page/Definitional%20Scheme) over that model. Since $T$ is stable, $M \models T$, and $p(x) \in S_x(M)$ is complete, we apply this result to $p$.
For every formula $\varphi(x;y)$, choose an $M$-definable predicate $d_p\varphi(y)$ such that, for every $m \in M^{|y|}$,
\begin{align*}
\varphi(x;m) \in p
\quad \iff \quad
\mathfrak C \models d_p\varphi(m).
\end{align*}
The cited theorem supplies the scheme in coherent form: for all formulas $\varphi(x;y)$ and $\psi(x;z)$, the predicates satisfy the Boolean compatibility conditions
\begin{align*}
d_p(\neg \varphi)(y) &\leftrightarrow \neg d_p\varphi(y),\\
d_p(\varphi \wedge \psi)(y,z) &\leftrightarrow d_p\varphi(y) \wedge d_p\psi(z)
\end{align*}
in $\mathfrak C$. Equivalently, Boolean connectives in the $x$-variable are interpreted by the corresponding Boolean operations on the defining predicates in the parameter variables. The displayed binary conjunction compatibility extends to any finite conjunction $\bigwedge_{i=1}^{r} \varphi_i(x;y_i)$ by induction on $r$, with the case $r=1$ immediate and the induction step obtained by applying the binary compatibility to $\bigwedge_{i=1}^{r-1} \varphi_i(x;y_i)$ and $\varphi_r(x;y_r)$. This preserves the defining equivalence over $M$ because $p$ is complete and therefore decides negations and finite conjunctions exactly as a complete Boolean ultrafilter of formulas over $M$.
[/step]
[step:Define a global type from the scheme and prove that it is complete and consistent]
Define a set of formulas over $\mathfrak C$ by
\begin{align*}
\tilde q(x)
:=
\{\,\varphi(x;c) : \varphi(x;y) \text{ is a formula},\ c \in \mathfrak C^{|y|},\ \mathfrak C \models d_p\varphi(c)\,\}.
\end{align*}
We first prove completeness. Let $\varphi(x;y)$ be a formula and let $c \in \mathfrak C^{|y|}$. By coherence,
\begin{align*}
d_p(\neg \varphi)(c) \leftrightarrow \neg d_p\varphi(c).
\end{align*}
Hence exactly one of $\mathfrak C \models d_p\varphi(c)$ and $\mathfrak C \models d_p(\neg\varphi)(c)$ holds. Therefore exactly one of $\varphi(x;c)$ and $\neg\varphi(x;c)$ belongs to $\tilde q$.
We next prove finite consistency. Let $\varphi_i(x;y_i)$ for $1 \le i \le r$ be formulas, let $c_i \in \mathfrak C^{|y_i|}$, and suppose $\varphi_i(x;c_i) \in \tilde q$ for each $i$. Define the conjunction formula
\begin{align*}
\theta(x;y_1,\dots,y_r) := \bigwedge_{i=1}^{r} \varphi_i(x;y_i).
\end{align*}
By coherence of the definitional scheme,
\begin{align*}
\mathfrak C \models d_p\theta(c_1,\dots,c_r).
\end{align*}
We claim that
\begin{align*}
\mathfrak C \models \exists x\,\theta(x;c_1,\dots,c_r).
\end{align*}
If not, then the $M$-definable formula
\begin{align*}
d_p\theta(y_1,\dots,y_r) \wedge \neg \exists x\,\theta(x;y_1,\dots,y_r)
\end{align*}
would be realized in $\mathfrak C$. Since $M \preceq \mathfrak C$ and all parameters occurring in $d_p\theta$ lie in $M$, elementarity gives tuples $m_i \in M^{|y_i|}$ such that
\begin{align*}
\mathfrak C \models d_p\theta(m_1,\dots,m_r)
\wedge
\neg \exists x\,\theta(x;m_1,\dots,m_r).
\end{align*}
The first conjunct implies $\theta(x;m_1,\dots,m_r) \in p$, by the defining property of $d_p\theta$ over $M$. Since $p$ is a complete type, every formula in $p$ is consistent with $T$ together with the elementary diagram of $M$, so
\begin{align*}
\mathfrak C \models \exists x\,\theta(x;m_1,\dots,m_r),
\end{align*}
contradicting the second conjunct. Thus every finite subset of $\tilde q$ is realized in $\mathfrak C$, so $\tilde q$ is consistent. By compactness, $\tilde q$ is consistent. Since the preceding completeness argument shows that $\tilde q$ decides every formula with parameters from $\mathfrak C$, this consistent set of formulas is a complete [global type](/page/Global%20Type) in $S_x(\mathfrak C)$.
[guided]
We define the proposed global extension by letting the same formulas that define $p$ over $M$ decide instances over the whole monster model. For every formula $\varphi(x;y)$ and every parameter tuple $c \in \mathfrak C^{|y|}$, put
\begin{align*}
\varphi(x;c) \in \tilde q
\quad \iff \quad
\mathfrak C \models d_p\varphi(c).
\end{align*}
Equivalently,
\begin{align*}
\tilde q(x)
=
\{\,\varphi(x;c) : \varphi(x;y) \text{ is a formula},\ c \in \mathfrak C^{|y|},\ \mathfrak C \models d_p\varphi(c)\,\}.
\end{align*}
The first point to verify is completeness. Fix a formula $\varphi(x;y)$ and a tuple $c \in \mathfrak C^{|y|}$. A complete type must decide exactly one of $\varphi(x;c)$ and $\neg\varphi(x;c)$. The coherence of the definitional scheme gives
\begin{align*}
d_p(\neg \varphi)(c) \leftrightarrow \neg d_p\varphi(c).
\end{align*}
Therefore exactly one of the two predicates $d_p\varphi(c)$ and $d_p(\neg\varphi)(c)$ holds in $\mathfrak C$. By the definition of $\tilde q$, exactly one of $\varphi(x;c)$ and $\neg\varphi(x;c)$ lies in $\tilde q$.
The second point is finite consistency. Suppose
\begin{align*}
\varphi_1(x;c_1),\dots,\varphi_r(x;c_r)
\end{align*}
are finitely many formulas from $\tilde q$, where each $\varphi_i(x;y_i)$ is a formula and each $c_i \in \mathfrak C^{|y_i|}$. We must prove that these formulas can be realized simultaneously. Define the conjunction
\begin{align*}
\theta(x;y_1,\dots,y_r) := \bigwedge_{i=1}^{r} \varphi_i(x;y_i).
\end{align*}
Because each $\varphi_i(x;c_i)$ belongs to $\tilde q$, we have
\begin{align*}
\mathfrak C \models d_p\varphi_i(c_i)
\end{align*}
for every $1 \le i \le r$. Coherence of the definitional scheme turns the separate decisions into a decision for the conjunction:
\begin{align*}
\mathfrak C \models d_p\theta(c_1,\dots,c_r).
\end{align*}
Now we prove that the conjunction is realized. Suppose toward a contradiction that
\begin{align*}
\mathfrak C \models \neg \exists x\,\theta(x;c_1,\dots,c_r).
\end{align*}
Then the tuple $(c_1,\dots,c_r)$ realizes the $M$-definable condition
\begin{align*}
d_p\theta(y_1,\dots,y_r) \wedge \neg \exists x\,\theta(x;y_1,\dots,y_r).
\end{align*}
All parameters in $d_p\theta$ lie in $M$. Since $M \preceq \mathfrak C$, elementarity transfers the existence of such a tuple from $\mathfrak C$ down to $M$. Hence there are tuples $m_i \in M^{|y_i|}$ such that
\begin{align*}
\mathfrak C \models d_p\theta(m_1,\dots,m_r)
\wedge
\neg \exists x\,\theta(x;m_1,\dots,m_r).
\end{align*}
The first conjunct says, by the defining property of the scheme over $M$, that
\begin{align*}
\theta(x;m_1,\dots,m_r) \in p.
\end{align*}
But $p$ is a complete type over $M$, so every formula in $p$ is consistent with the elementary diagram of $M$. Therefore
\begin{align*}
\mathfrak C \models \exists x\,\theta(x;m_1,\dots,m_r),
\end{align*}
which contradicts the second conjunct. This proves that every finite subset of $\tilde q$ is satisfiable in $\mathfrak C$. By compactness, $\tilde q$ is consistent. Since we already proved that $\tilde q$ decides every formula with parameters from $\mathfrak C$, this consistent set of formulas is a complete global type over $\mathfrak C$.
[/guided]
[/step]
[step:Show that the global type extends $p$]
Let $\varphi(x;y)$ be a formula and let $m \in M^{|y|}$. By the definition of $\tilde q$ and by the defining property of $d_p\varphi$ over $M$,
\begin{align*}
\varphi(x;m) \in \tilde q
&\iff \mathfrak C \models d_p\varphi(m)\\
&\iff \varphi(x;m) \in p.
\end{align*}
Thus $\tilde q|_M = p$.
[/step]
[step:Use $M$-definability to prove $M$-invariance]
Let $\sigma \in \operatorname{Aut}(\mathfrak C/M)$ be an automorphism fixing $M$ pointwise. Let $\varphi(x;y)$ be a formula and let $c \in \mathfrak C^{|y|}$. Since $d_p\varphi(y)$ is $M$-definable and $\sigma$ fixes every parameter from $M$, satisfaction of $d_p\varphi$ is preserved under $\sigma$:
\begin{align*}
\mathfrak C \models d_p\varphi(c)
\quad \iff \quad
\mathfrak C \models d_p\varphi(\sigma(c)).
\end{align*}
Using the definition of $\tilde q$ on both sides gives
\begin{align*}
\varphi(x;c) \in \tilde q
\quad \iff \quad
\varphi(x;\sigma(c)) \in \tilde q.
\end{align*}
Therefore $\tilde q$ is $M$-[invariant](/page/Invariant%20Type).
[guided]
We prove invariance by checking the defining condition for an $M$-invariant type. Let $\sigma \in \operatorname{Aut}(\mathfrak C/M)$ be an automorphism fixing every element of $M$, let $\varphi(x;y)$ be a formula, and let $c \in \mathfrak C^{|y|}$. The predicate $d_p\varphi(y)$ is $M$-definable, meaning that all parameters appearing in it are from $M$. Since $\sigma$ fixes those parameters pointwise, applying $\sigma$ preserves the truth of this predicate:
\begin{align*}
\mathfrak C \models d_p\varphi(c)
\quad \iff \quad
\mathfrak C \models d_p\varphi(\sigma(c)).
\end{align*}
Now translate both sides back into membership in $\tilde q$ using the definition of the global type. The left side is equivalent to $\varphi(x;c) \in \tilde q$, and the right side is equivalent to $\varphi(x;\sigma(c)) \in \tilde q$. Thus
\begin{align*}
\varphi(x;c) \in \tilde q
\quad \iff \quad
\varphi(x;\sigma(c)) \in \tilde q.
\end{align*}
This is exactly invariance under automorphisms fixing $M$, so $\tilde q$ is $M$-[invariant](/page/Invariant%20Type).
[/guided]
[/step]
[step:Restrict the global type to $B = M \cup A$]
Define
\begin{align*}
q := \tilde q|_B.
\end{align*}
Since $\tilde q \in S_x(\mathfrak C)$ is complete, its restriction to the parameter set $B$ is a complete type in $S_x(B)$. Since $M \subseteq B$ and $\tilde q|_M = p$, we have
\begin{align*}
q|_M = (\tilde q|_B)|_M = \tilde q|_M = p.
\end{align*}
Thus $q$ extends $p$.
The type $q$ inherits its intended invariance through the global type $\tilde q$: if $\sigma \in \operatorname{Aut}(\mathfrak C/M)$ and $c \in B^{|y|}$ with $\sigma(c) \in B^{|y|}$, then
\begin{align*}
\varphi(x;c) \in q
&\iff \varphi(x;c) \in \tilde q\\
&\iff \varphi(x;\sigma(c)) \in \tilde q\\
&\iff \varphi(x;\sigma(c)) \in q.
\end{align*}
This proves that $q$ is the restriction to $B$ of the [global type](/page/Global%20Type) $\tilde q$, which is $M$-[invariant](/page/Invariant%20Type) and was built from the $M$-[definitional scheme](/page/Definitional%20Scheme) for $p$.
[guided]
The theorem asks for a type over the smaller parameter set $B = M \cup A$, not necessarily for the whole global type. We therefore define
\begin{align*}
q := \tilde q|_B.
\end{align*}
Because $\tilde q$ is a complete type over $\mathfrak C$, its restriction to formulas with parameters from $B$ is a complete type over $B$, so $q \in S_x(B)$. Since $M \subseteq B$, restricting first to $B$ and then to $M$ gives the same result as restricting directly to $M$:
\begin{align*}
q|_M = (\tilde q|_B)|_M = \tilde q|_M = p.
\end{align*}
Thus $q$ is an extension of $p$ from $M$ to $B$.
Finally, the promised invariance is inherited from the global type rather than proved as an independent property of an arbitrary type over $B$. If $\sigma \in \operatorname{Aut}(\mathfrak C/M)$ and $c \in B^{|y|}$ with $\sigma(c) \in B^{|y|}$, then membership in $q$ is the same as membership in $\tilde q$ for formulas whose parameters are in $B$. Therefore
\begin{align*}
\varphi(x;c) \in q
&\iff \varphi(x;c) \in \tilde q\\
&\iff \varphi(x;\sigma(c)) \in \tilde q\\
&\iff \varphi(x;\sigma(c)) \in q.
\end{align*}
The middle equivalence is exactly the $M$-invariance of $\tilde q$ proved above. Hence $q$ is the restriction to $B$ of a global $M$-[invariant](/page/Invariant%20Type) type constructed from the $M$-[definitional scheme](/page/Definitional%20Scheme) for $p$, which is the conclusion of the theorem.
[/guided]
[/step]
