[proofplan]
We work inside a sufficiently saturated and strongly homogeneous monster model $\mathfrak{C} \models T$, and all parameter sets are understood to be small subsets of $\mathfrak{C}$. The general [stable forking calculus](/page/Forking%20Independence) gives invariance, base/right monotonicity, symmetry, transitivity, and extension for the relation $a \mathrel{\perp}_C B$ defined by non-forking of $\operatorname{tp}(a/BC)$ over $C$. The last assertion follows by applying the definition of a [stationary type](/page/Stationary%20Type) over a model: a stationary type over $M$ has exactly one non-forking extension to every parameter set containing $M$.
[/proofplan]
[step:Place the theorem inside a monster model and fix the independence notation]
Let $\mathfrak{C} \models T$ be a monster model, meaning that $\mathfrak{C}$ is sufficiently saturated and strongly homogeneous for all small parameter sets under discussion. For small sets $A,B,C \subset \mathfrak{C}$, write
\begin{align*}
A \mathrel{\perp}_C B
\end{align*}
to mean that for every finite tuple $a$ from $A$, the complete type $\operatorname{tp}(a/BC)$ does not fork over $C$. This is the standard forking-independence relation of the complete theory $T$.
For any small parameter set $E \subset \mathfrak{C}$, let $S(E)$ denote the space of complete types over $E$ in the variables under discussion. Because $T$ is complete, every tuple from $\mathfrak{C}$ has a well-defined complete type over every small parameter set. Because $T$ is stable, the [stable forking calculus](/page/Forking%20Independence) applies to this relation on small subsets of $\mathfrak{C}$. A type $p(x) \in S(M)$ is called stationary when it has a unique non-forking extension to $S(E)$ for every small parameter set $E \supset M$.
[/step]
[step:Apply the stable forking calculus to obtain the structural properties]
By the [stable forking calculus](/page/Forking%20Independence) for complete stable theories, the relation $\perp$ defined above satisfies the following five properties on small subsets of $\mathfrak{C}$:
For invariance, if $\sigma \in \operatorname{Aut}(\mathfrak{C})$ and $A \mathrel{\perp}_C B$, then
\begin{align*}
\sigma(A) \mathrel{\perp}_{\sigma(C)} \sigma(B).
\end{align*}
For monotonicity, if $A \mathrel{\perp}_C BD$, where $BD$ denotes $B \cup D$, then both
\begin{align*}
A \mathrel{\perp}_C B
\end{align*}
and
\begin{align*}
A \mathrel{\perp}_{BC} D
\end{align*}
hold, where $BC$ denotes $B \cup C$.
For symmetry, if $A \mathrel{\perp}_C B$, then
\begin{align*}
B \mathrel{\perp}_C A.
\end{align*}
For transitivity, if $C \subset D \subset B$, then
\begin{align*}
A \mathrel{\perp}_C B
\end{align*}
holds if and only if both
\begin{align*}
A \mathrel{\perp}_C D
\end{align*}
and
\begin{align*}
A \mathrel{\perp}_D B
\end{align*}
hold. For existence of non-forking extensions, if $p(x) \in S(C)$ is a complete type and $B \supset C$ is small, then there is some $q(x) \in S(B)$ extending $p$ such that $q$ does not fork over $C$.
[guided]
The purpose of passing to the monster model is to make the independence relation uniform: all sets and tuples live in one ambient structure $\mathfrak{C}$. We define $A \mathrel{\perp}_C B$ by requiring that each finite tuple $a$ from $A$ has type $\operatorname{tp}(a/BC)$ non-forking over $C$. This converts the type-theoretic notion of non-forking into a relation between parameter sets.
Now the hypothesis that $T$ is stable is used. The [stable forking calculus](/page/Forking%20Independence) says precisely that, for a complete stable theory, non-forking independence satisfies the formal calculus expected of independence. Its hypotheses are met here: $T$ is complete and stable by the theorem statement, and all sets named in the step are small subsets of the monster model.
The theorem gives invariance because automorphisms of $\mathfrak{C}$ preserve complete types and preserve whether a formula forks over a base. Thus, from $A \mathrel{\perp}_C B$ and $\sigma \in \operatorname{Aut}(\mathfrak{C})$, we obtain
\begin{align*}
\sigma(A) \mathrel{\perp}_{\sigma(C)} \sigma(B).
\end{align*}
It gives monotonicity in the base/right form needed here. Suppose $A \mathrel{\perp}_C BD$, where $BD$ denotes $B \cup D$. Right monotonicity gives
\begin{align*}
A \mathrel{\perp}_C B.
\end{align*}
Base monotonicity, applied with the enlarged base $BC = B \cup C$ and the remaining right-hand parameters $D$, gives
\begin{align*}
A \mathrel{\perp}_{BC} D.
\end{align*}
Thus the single independence statement $A \mathrel{\perp}_C BD$ decomposes into both conclusions required by monotonicity.
It gives symmetry because stable forking is symmetric between the two independent sides, so
\begin{align*}
A \mathrel{\perp}_C B \implies B \mathrel{\perp}_C A.
\end{align*}
It gives transitivity because independence over an intermediate base $D$ with $C \subset D \subset B$ decomposes into independence from $D$ over $C$ and independence from $B$ over $D$:
\begin{align*}
A \mathrel{\perp}_C B
\end{align*}
holds if and only if both
\begin{align*}
A \mathrel{\perp}_C D
\end{align*}
and
\begin{align*}
A \mathrel{\perp}_D B
\end{align*}
hold. Finally, it gives extension: for every complete type $p(x) \in S(C)$ and every small $B \supset C$, there exists an extension $q(x) \in S(B)$ of $p$ such that $q$ does not fork over $C$. These are exactly the first five assertions in the theorem statement.
[/guided]
[/step]
[step:Use stationarity over a model to prove uniqueness of non-forking extensions]
Let $M \models T$ be a model, let $p(x) \in S(M)$ be stationary, and let $B \supset M$ be a small parameter set. By existence of non-forking extensions from the [stable forking calculus](/page/Forking%20Independence), there is at least one type $q(x) \in S(B)$ extending $p$ such that $q$ does not fork over $M$.
Since $p$ is a [stationary type](/page/Stationary%20Type), by definition $p$ has at most one non-forking extension to any small parameter set containing $M$. Applying this definition to the parameter set $B$, any two types $q_1(x),q_2(x) \in S(B)$ extending $p$ and not forking over $M$ must satisfy
\begin{align*}
q_1 = q_2.
\end{align*}
Therefore the non-forking extension of $p$ to $S(B)$ exists and is unique.
[/step]
[step:Collect the conclusions]
The stable forking calculus proves invariance, monotonicity, symmetry, transitivity, and existence of non-forking extensions for forking independence in the complete stable theory $T$. The stationarity of $p(x) \in S(M)$, together with existence, proves that for every small parameter set $B \supset M$ there is a unique non-forking extension of $p$ to $S(B)$. This is precisely the theorem statement.
[/step]
