Every linear subspace $U$ of a vector space $V$ has a complement: a linear subspace $W$ with $V=U\oplus W$

Given: The Axiom of Choice; a field $F$; a vector space $V$ over $F$; and a linear subspace $U$ of $V$.

$U$ is itself a vector space over $F$, with the addition, the zero and the scalar multiplication of $V$ (Linear subspace of a vector space); every vector space has a basis (Every vector space has a basis); and for $A\subseteq U$, "$A$ is a basis of $U$" means $A$ is linearly independent as a subset of $V$ with $\mathrm{span}(A)=U$ (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, section on bases of a linear subspace, Linear independence: a finite list $v:n\to V$ is independent when ${\sum }_{i<n}{\lambda }_i{v}_i=0_V$ forces every ${\lambda }_i=0_F$, and a subset $S\subseteq V$ is independent when every injective finite list into $S$ is independent).

If $L\subseteq S\subseteq V$ with $L$ linearly independent and $\mathrm{span}(S)=V$, there is a basis $B$ of $V$ with $L\subseteq B\subseteq S$; and $\mathrm{span}(V)=V$ (Zorn's lemma gives a basis between any linearly independent set and any spanning set containing it: if $L\subseteq S\subseteq V$ with $L$ independent and $\mathrm{span}(S)=V$, there is a basis $B$ of $V$ with $L\subseteq B\subseteq S$, The span is monotone and idempotent, $\mathrm{span}(S)=S$ exactly when $S$ is a linear subspace, and $\mathrm{span}(S\cup \{0_V\})=\mathrm{span}(S)$, claim 4).

$\mathrm{span}(T)$ is a linear subspace of $V$ containing $T$, contained in every linear subspace of $V$ containing $T$, and monotone in $T$ (Linear combination of a finite list, and the span $\mathrm{span}(S)$ as the smallest linear subspace containing $S$, The span is monotone and idempotent, $\mathrm{span}(S)=S$ exactly when $S$ is a linear subspace, and $\mathrm{span}(S\cup \{0_V\})=\mathrm{span}(S)$, $\mathrm{span}(S)$ is exactly the set of linear combinations of finite lists of elements of $S$, and $\mathrm{span}(\mathrm{\varnothing })=\{0_V\}$).

For two linear subspaces, $U+W={\sum }_{i<2}{U}_i$ and ${\sum }_{i<2}{U}_i=\mathrm{span}(U\cup W)$ (The sum $U+W$ of two linear subspaces and the sum ${\sum }_{i<n}{U}_i$ of a finite family, ${\sum }_{i<n}{U}_i=\mathrm{span}\left({\bigcup }_{i<n}{U}_i\right)$, so the sum is the smallest linear subspace containing every $U_i$).

$\mathrm{span}(T)$ is already the set of ${\sum }_{i<p}{\alpha }_i{a}_i$ with $a:p\to T$ injective (A subset $S\subseteq V$ is linearly dependent if and only if some $s\in S$ lies in $\mathrm{span}(S\setminus \{s\})$; and $\mathrm{span}(S)$ is already the set of linear combinations of INJECTIVE finite lists into $S$, claim 2).

Concatenation: for $y:p\to X$ and $z:q\to X$ there is exactly one $c:p+q\to X$ with $c_i=y_i$ for $i<p$ and $c_{p+j}=z_j$ for $j<q$; when $X=V$ it satisfies ${\sum }_{i<p+q}{c}_i={\sum }_{i<p}{y}_i+{\sum }_{j<q}{z}_j$; and if $y$ and $z$ are injective with disjoint images then $c$ is injective with image $y[p]\cup z[q]$. A list into $V$ is linearly independent exactly when it is injective with linearly independent image (Finite sums re-indexed along an injection, with a zero term deleted, and concatenated; and the closure properties of linear independence: an independent list is injective and never $0_V$, its sublists are independent, a list is independent exactly when it is injective with linearly independent image, and every subset of a linearly independent set is linearly independent, claims 3 and 6). The scalar case is the same statement read in $F$, a vector space over itself (A field is a vector space over itself, and over any subfield $K\subseteq F$ every $F$-vector space is a $K$-vector space by restricting the scalars, claim 1).

$(V,+,0_V)$ is an abelian group; $0_{F}y=0_V$; $(-1_F)y=-y$; (V4) $(\lambda \mu )y=\lambda (\mu y)$; (F1) an all-$0_V$ list sums to $0_V$; and a scalar passes through a finite sum, so $(-1_F){\sum }_{j<q}{\beta }_j{b}_j={\sum }_{j<q}(-{\beta }_j)b_j$ (Vector space over a field, In any vector space $0_{F}v=0_V$, $\lambda 0_V=0_V$, $(-\lambda )v=-(\lambda v)$, $(-1_F)v=-v$, and $\lambda v=0_V$ forces $\lambda =0_F$ or $v=0_V$, Field, The sum $U+W$ of two linear subspaces and the sum ${\sum }_{i<n}{U}_i$ of a finite family, The product $g_0{g}_1\cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ($n=0$) equal to the identity).

Indices run over von Neumann naturals (The natural numbers $\mathbb{N}$ (von Neumann), On $\mathbb{N}$ the order is membership: $m<n⟺m\in n$) and injectivity is as in Injection, surjection, bijection.