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 $\mathrm{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=\mathrm{span}(A)$. But $y\in A_W$ means $y\mathrm{\notin }A$, so $A\subseteq B_W\setminus \{y\}$ and monotonicity gives $y\in \mathrm{span}(A)\subseteq \mathrm{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^{\mathrm{\prime }}$ 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^{\mathrm{\prime }}$ 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=\left({\sum }_{i<a+q}{\gamma }_i{c}_i^{\mathrm{\prime }}\right)+\left({\sum }_{k<r}{\gamma }_{(a+q)+k}{\delta }_k\right)$.

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^{\mathrm{\prime }}$ 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^{\mathrm{\prime }}$, whose values lie in $B_U$, so $P\in \mathrm{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 \mathrm{span}(B_W)=W$. Hence $R\in U\cap W=\mathrm{span}(A)=\mathrm{span}(\alpha [a])$, so $R={\sum }_{i<a}{\epsilon }_i{\alpha }_i$ for some $\epsilon :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 $\epsilon$ 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 ${\epsilon }_i=0_F$ for every $i<a$, whence $R=0_V$ by (F1) and $P=-R=0_V$. Finally $c^{\mathrm{\prime }}$ 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.

$\mathrm{span}(C)=U+W$. From $B_U\subseteq C$ and $B_W\subseteq C$ and monotonicity, $U=\mathrm{span}(B_U)\subseteq \mathrm{span}(C)$ and $W=\mathrm{span}(B_W)\subseteq \mathrm{span}(C)$, so $U\cup W\subseteq \mathrm{span}(C)$ and hence $U+W=\mathrm{span}(U\cup W)\subseteq \mathrm{span}(C)$. Conversely $C=B_U\cup B_W\subseteq U\cup W\subseteq U+W$, and $U+W$ is a linear subspace, so $\mathrm{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}$.