[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.[/step]

[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: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]