The dimension formula: for finite-dimensional linear subspaces $U$ and $W$ of $V$, the subspaces $U + W$ and $U \cap W$ are finite-dimensional and $\dim_F(U+W) + \dim_F(U \cap W) = \dim_F U + \dim_F W$

$U \cap W$ is a linear subspace of $V$ contained in $U$, hence a linear subspace of $U$; since $U$ is finite-dimensional, so is $U \cap W$. Write $a := \dim_F(U \cap W)$, fix a basis $A$ of $U \cap W$ with $A \approx a$, and fix an injective list $\alpha : a \to V$ with image $A$. Note $\operatorname{span}(A) = U \cap W$, and that independence and spans may be computed in $V$ throughout.

Extending $A$ in each of $U$ and $W$. The set $A$ is linearly independent with $A \subseteq U$, and $U$ is finite-dimensional, so $A$ is contained in a basis $B_U$ of $U$; likewise $A \subseteq W$ gives a basis $B_W$ of $W$ with $A \subseteq B_W$. Both extensions are the finite-dimensional ones, with no appeal to Zorn's lemma. Put $A_U := B_U \setminus A$ and $A_W := B_W \setminus A$, which are disjoint from $A$ by construction. Each is a subset of a linearly independent set, hence linearly independent, and each lies in a space with a finite basis, hence is finite; fix $q$ and $r$ with $A_U \approx q$ and $A_W \approx r$, and injective lists $\beta : q \to V$ with image $A_U$ and $\delta : r \to V$ with image $A_W$.

The sizes add up. The lists $\alpha$ and $\beta$ are injective with disjoint images, so their concatenation is an injective list $a+q \to V$ with image $A \cup A_U = B_U$; hence $B_U \approx a + q$. Also $B_U$ is a basis of $U$, so $B_U \approx u$, and a finite set is equinumerous with exactly one natural number, so $a + q = u$. The same argument with $\delta$ gives $a + r = w$.

$A_U$ and $A_W$ are disjoint. Suppose $y \in A_U \cap A_W$. Then $y \in B_U \subseteq U$ and $y \in B_W \subseteq W$, so $y \in U \cap W = \operatorname{span}(A)$. But $y \in A_W$ means $y \notin A$, so $A \subseteq B_W \setminus \{y\}$ and monotonicity gives $y \in \operatorname{span}(A) \subseteq \operatorname{span}(B_W \setminus \{y\})$, which makes $B_W$ linearly dependent and contradicts its being a basis.

One list carrying all three blocks. Let $c'$ be the concatenation of $\alpha$ and $\beta$, an injective list $a+q \to V$ with image $B_U$, and let $c$ be the concatenation of $c'$ and $\delta$, a list $(a+q)+r \to V$. By step 3.2 the images $B_U$ and $A_W$ are disjoint, since $B_U \cap A_W$ would lie in $A \cap A_W$ or in $A_U \cap A_W$, both empty; so $c$ is injective with image $C := B_U \cup A_W = A \cup A_U \cup A_W = B_U \cup B_W$. For scalars $\gamma : (a+q)+r \to F$ the sum splits as $\sum_{i<(a+q)+r}\gamma_i c_i = \bigl(\sum_{i<a+q}\gamma_i c'_i\bigr) + \bigl(\sum_{k<r}\gamma_{(a+q)+k}\delta_k\bigr)$.

The list $c$ is linearly independent. Let $\gamma : (a+q)+r \to F$ with $\sum_{i<(a+q)+r}\gamma_i c_i = 0_V$, and write $P := \sum_{i<a+q}\gamma_i c'_i$ and $R := \sum_{k<r}\gamma_{(a+q)+k}\delta_k$, so $P + R = 0_V$ by step 4.1 and hence $R = -P$. Now $P$ is a linear combination of the list $c'$, whose values lie in $B_U$, so $P \in \operatorname{span}(B_U) = U$ and therefore $R = -P \in U$; and $R$ is a linear combination of $\delta$, whose values lie in $A_W \subseteq B_W$, so $R \in \operatorname{span}(B_W) = W$. Hence $R \in U \cap W = \operatorname{span}(A) = \operatorname{span}(\alpha[a])$, so $R = \sum_{i<a}\varepsilon_i\alpha_i$ for some $\varepsilon : a \to F$. Let $d$ be the concatenation of $\alpha$ and $\delta$, injective with image $A \cup A_W = B_W$ since $A$ and $A_W$ are disjoint, and let $\eta$ be the concatenation of $\varepsilon$ with $k \mapsto -\gamma_{(a+q)+k}$; then $\sum_{i<a+r}\eta_i d_i = R + (-R) = 0_V$. As $d$ is an injective list into the linearly independent set $B_W$, it is a linearly independent list, so every $\eta_i = 0_F$; in particular $\gamma_{(a+q)+k} = 0_F$ for every $k < r$, and $\varepsilon_i = 0_F$ for every $i < a$, whence $R = 0_V$ by (F1) and $P = -R = 0_V$. Finally $c'$ is an injective list into the linearly independent set $B_U$, hence linearly independent, so $P = 0_V$ forces $\gamma_i = 0_F$ for every $i < a+q$. Every coefficient of $\gamma$ therefore vanishes.

$\operatorname{span}(C) = U + W$. From $B_U \subseteq C$ and $B_W \subseteq C$ and monotonicity, $U = \operatorname{span}(B_U) \subseteq \operatorname{span}(C)$ and $W = \operatorname{span}(B_W) \subseteq \operatorname{span}(C)$, so $U \cup W \subseteq \operatorname{span}(C)$ and hence $U + W = \operatorname{span}(U \cup W) \subseteq \operatorname{span}(C)$. Conversely $C = B_U \cup B_W \subseteq U \cup W \subseteq U + W$, and $U + W$ is a linear subspace, so $\operatorname{span}(C) \subseteq U + W$.

$C$ is a basis of $U + W$ with $(a+q)+r$ elements. By step 5.1 the list $c$ is linearly independent, hence injective with linearly independent image $C$ and $C \approx (a+q)+r$; by step 5.2 it spans $U + W$. So $U + W$ is finite-dimensional with $\dim_F(U+W) = (a+q)+r$.

The formula. By step 3.1, $a + q = u$ and $a + r = w$, so step 6.1 gives $\dim_F(U+W) = u + r$, and with $\dim_F(U \cap W) = a$ from step 1.1 we get $\dim_F(U+W) + \dim_F(U \cap W) = (u + r) + a = u + (r + a) = u + (a + r) = u + w = \dim_F U + \dim_F W$, using associativity and commutativity of addition on $\mathbb{N}$.