[proofplan]
Choose a basis of $U\cap W$, then extend it separately to bases of $U$ and $W$. The combined list of the intersection basis together with the two extension lists will be shown to span $U+W$ and to be linearly independent. Once this list is a basis of $U+W$, counting its vectors gives the dimension formula, with the intersection basis counted once rather than twice.
[/proofplan]
[step:Choose a basis of the intersection and extend it inside each subspace]
Since $V$ is finite-dimensional and $U,W \subset V$ are subspaces, the subspaces $U$, $W$, and $U\cap W$ are finite-dimensional. Let
\begin{align*}
(e_1,\dots,e_r)
\end{align*}
be a basis of $U\cap W$, where $r$ is a nonnegative integer. By the finite-dimensional basis extension argument inside $U$, choose vectors $a_1,\dots,a_s \in U$ such that
\begin{align*}
(e_1,\dots,e_r,a_1,\dots,a_s)
\end{align*}
is a basis of $U$. Similarly, choose vectors $b_1,\dots,b_t \in W$ such that
\begin{align*}
(e_1,\dots,e_r,b_1,\dots,b_t)
\end{align*}
is a basis of $W$.
Here $s$ and $t$ are nonnegative integers, and the corresponding added list is empty when $s=0$ or $t=0$.
[/step]
[step:Show the combined list spans the sum $U+W$]
Define the combined list
\begin{align*}
\mathcal C=(e_1,\dots,e_r,a_1,\dots,a_s,b_1,\dots,b_t).
\end{align*}
We show that $\operatorname{span}_F(\mathcal C)=U+W$.
First, every vector in $\mathcal C$ belongs to $U+W$: each $e_i$ lies in $U\cap W \subset U$, each $a_j$ lies in $U$, and each $b_k$ lies in $W$. Hence
\begin{align*}
\operatorname{span}_F(\mathcal C)\subset U+W.
\end{align*}
Conversely, let $x\in U+W$. By the definition of the subspace sum, there exist $u\in U$ and $w\in W$ such that
\begin{align*}
x=u+w.
\end{align*}
Because $(e_1,\dots,e_r,a_1,\dots,a_s)$ is a basis of $U$, there exist scalars $\alpha_1,\dots,\alpha_r,\lambda_1,\dots,\lambda_s\in F$ such that
\begin{align*}
u=\sum_{i=1}^{r}\alpha_i e_i+\sum_{j=1}^{s}\lambda_j a_j.
\end{align*}
Because $(e_1,\dots,e_r,b_1,\dots,b_t)$ is a basis of $W$, there exist scalars $\beta_1,\dots,\beta_r,\mu_1,\dots,\mu_t\in F$ such that
\begin{align*}
w=\sum_{i=1}^{r}\beta_i e_i+\sum_{k=1}^{t}\mu_k b_k.
\end{align*}
Adding these two expressions gives
\begin{align*}
x=\sum_{i=1}^{r}(\alpha_i+\beta_i)e_i+\sum_{j=1}^{s}\lambda_j a_j+\sum_{k=1}^{t}\mu_k b_k.
\end{align*}
Thus $x\in \operatorname{span}_F(\mathcal C)$, and therefore
\begin{align*}
U+W\subset \operatorname{span}_F(\mathcal C).
\end{align*}
So $\mathcal C$ spans $U+W$.
[/step]
[step:Prove the combined list is linearly independent]
Suppose scalars $\gamma_1,\dots,\gamma_r,\lambda_1,\dots,\lambda_s,\mu_1,\dots,\mu_t\in F$ satisfy
\begin{align*}
\sum_{i=1}^{r}\gamma_i e_i+\sum_{j=1}^{s}\lambda_j a_j+\sum_{k=1}^{t}\mu_k b_k=0_V.
\end{align*}
Move the $W$-extension terms to the other side:
\begin{align*}
\sum_{i=1}^{r}\gamma_i e_i+\sum_{j=1}^{s}\lambda_j a_j=-\sum_{k=1}^{t}\mu_k b_k.
\end{align*}
The left-hand side belongs to $U$, since each $e_i$ and each $a_j$ belongs to $U$. The right-hand side belongs to $W$, since each $b_k$ belongs to $W$. Hence the common vector belongs to $U\cap W$.
Because $(e_1,\dots,e_r)$ is a basis of $U\cap W$, there exist scalars $\delta_1,\dots,\delta_r\in F$ such that
\begin{align*}
\sum_{i=1}^{r}\gamma_i e_i+\sum_{j=1}^{s}\lambda_j a_j=\sum_{i=1}^{r}\delta_i e_i.
\end{align*}
Subtracting the right-hand side gives a linear relation among the basis vectors of $U$:
\begin{align*}
\sum_{i=1}^{r}(\gamma_i-\delta_i)e_i+\sum_{j=1}^{s}\lambda_j a_j=0_V.
\end{align*}
Since $(e_1,\dots,e_r,a_1,\dots,a_s)$ is linearly independent, we obtain
\begin{align*}
\lambda_1=\cdots=\lambda_s=0.
\end{align*}
Returning to the original relation, we now have
\begin{align*}
\sum_{i=1}^{r}\gamma_i e_i+\sum_{k=1}^{t}\mu_k b_k=0_V.
\end{align*}
Since $(e_1,\dots,e_r,b_1,\dots,b_t)$ is linearly independent, all remaining coefficients vanish:
\begin{align*}
\gamma_1=\cdots=\gamma_r=0
\end{align*}
and
\begin{align*}
\mu_1=\cdots=\mu_t=0.
\end{align*}
Thus every linear relation among the vectors of $\mathcal C$ is trivial, so $\mathcal C$ is linearly independent.
[guided]
We want to prove that the list
\begin{align*}
\mathcal C=(e_1,\dots,e_r,a_1,\dots,a_s,b_1,\dots,b_t)
\end{align*}
is linearly independent. The only possible difficulty is that the $a_j$ vectors live in $U$ and the $b_k$ vectors live in $W$, so a relation might mix the two subspaces. The way to control this mixing is to isolate a vector that lies in both $U$ and $W$, and then express it using the basis of the intersection.
Assume that scalars $\gamma_1,\dots,\gamma_r,\lambda_1,\dots,\lambda_s,\mu_1,\dots,\mu_t\in F$ satisfy
\begin{align*}
\sum_{i=1}^{r}\gamma_i e_i+\sum_{j=1}^{s}\lambda_j a_j+\sum_{k=1}^{t}\mu_k b_k=0_V.
\end{align*}
Rearrange the equation by moving the $b_k$ terms to the other side:
\begin{align*}
\sum_{i=1}^{r}\gamma_i e_i+\sum_{j=1}^{s}\lambda_j a_j=-\sum_{k=1}^{t}\mu_k b_k.
\end{align*}
The left-hand side is an element of $U$, because $e_i\in U\cap W\subset U$ and $a_j\in U$. The right-hand side is an element of $W$, because each $b_k\in W$ and $W$ is closed under finite linear combinations. Therefore this common vector lies in $U\cap W$.
Now use the fact that $(e_1,\dots,e_r)$ is a basis of $U\cap W$. Since the common vector belongs to $U\cap W$, there are scalars $\delta_1,\dots,\delta_r\in F$ such that
\begin{align*}
\sum_{i=1}^{r}\gamma_i e_i+\sum_{j=1}^{s}\lambda_j a_j=\sum_{i=1}^{r}\delta_i e_i.
\end{align*}
Subtracting the right-hand side produces a linear relation in the basis of $U$:
\begin{align*}
\sum_{i=1}^{r}(\gamma_i-\delta_i)e_i+\sum_{j=1}^{s}\lambda_j a_j=0_V.
\end{align*}
Since $(e_1,\dots,e_r,a_1,\dots,a_s)$ is a basis of $U$, it is linearly independent. Hence every coefficient in this relation is zero, and in particular
\begin{align*}
\lambda_1=\cdots=\lambda_s=0.
\end{align*}
Substituting these equalities back into the original relation leaves
\begin{align*}
\sum_{i=1}^{r}\gamma_i e_i+\sum_{k=1}^{t}\mu_k b_k=0_V.
\end{align*}
This is now a linear relation among the basis vectors of $W$, namely among the list $(e_1,\dots,e_r,b_1,\dots,b_t)$. Since that list is linearly independent, all its coefficients are zero:
\begin{align*}
\gamma_1=\cdots=\gamma_r=0
\end{align*}
and
\begin{align*}
\mu_1=\cdots=\mu_t=0.
\end{align*}
We have shown that every coefficient in the original relation is zero. Therefore $\mathcal C$ is linearly independent.
[/guided]
[/step]
[step:Count the vectors in the constructed basis]
The preceding two steps show that $\mathcal C$ is a basis of $U+W$. Therefore
\begin{align*}
\dim(U+W)=r+s+t.
\end{align*}
By construction,
\begin{align*}
\dim(U\cap W)=r,
\end{align*}
\begin{align*}
\dim U=r+s,
\end{align*}
and
\begin{align*}
\dim W=r+t.
\end{align*}
Consequently,
\begin{align*}
\dim U+\dim W-\dim(U\cap W)=(r+s)+(r+t)-r=r+s+t.
\end{align*}
Combining this equality with $\dim(U+W)=r+s+t$ gives
\begin{align*}
\dim(U+W)=\dim U+\dim W-\dim(U\cap W).
\end{align*}
This is the desired dimension formula.
[/step]
