The coordinate vector space over F2

The coordinate operations are closed because each coordinate operation is an operation in ${\mathbb{F}}_2$ by [F1]. Each vector-space axiom in [F2] holds coordinate by coordinate by the corresponding field axiom in [F1]; coordinatewise equality then gives the vector identity. For $n=0$ there is only the empty tuple, and all coordinate identities hold vacuously.

For $i<n$, let $e_i$ have coordinate $1$ at $i$ and $0$ elsewhere. Every $x\in {\mathbb{F}}_2^n$ equals ${\sum }_{i<n}{x}_i{e}_i$ coordinatewise, so $B=\{e_i:i<n\}$ spans. The vectors $e_i$ are pairwise distinct because their $1$-coordinates differ. To verify that $B$ is independent in the subset sense of [F3], take any finite injective list $b:r\to B$ and coefficients $c_t\in {\mathbb{F}}_2$. If $r=0$, the independence implication is vacuous. Otherwise write $b_t=e_{i_t}$; injectivity and distinctness of the $e_i$ make the indices $i_t$ pairwise distinct. The coordinate $i_t$ of ${\sum }_{u<r}{c}_u{b}_u$ is then exactly $c_t$, so a zero sum forces every $c_t=0$. This also covers $n=0$, since then $B=\mathrm{\varnothing }$ admits no nonempty list. Thus $B$ is independent, and it is a basis by [F4]–[F5]. Its $n$ distinct vectors give dimension $n$.