The standard list $e:n\to F^n$ with $e_i(i)=1_F$ and $e_i(j)=0_F$ for $j\mathrm{\ne }i$ is an ordered basis of $F^n$; hence ${\dim }_F{F}^n=n$, and $F^0$ is the zero space with basis $\mathrm{\varnothing }$ and dimension $0$

Let $F$ be a field (Field), let $n\in \mathbb{N}$ and let $F^n$ be the function space on the von Neumann natural $n=\{0,\dots ,n-1\}$, with the pointwise operations (The vector space $F^X$ of all functions $X\to F$ with pointwise operations, and $F^n$ as the case $X=n=\{0,1,\dots ,n-1\}$, The natural numbers $\mathbb{N}$ (von Neumann), On $\mathbb{N}$ the order is membership: $m<n⟺m\in n$). For $i<n$ define the standard unit vector $e_i\in F^n$ by

$e_i(i)=1_F,e_i(j)=0_F\text{ for }j<n\text{ with }j\mathrm{\ne }i\mathrm{.}$

Then:

1. Finite sums in a function space are pointwise. For every set $X$, every $p\in \mathbb{N}$, every list $u:p\to F^X$ and every $j\in X$, $\left({\sum }_{k<p}{u}_k\right)(j)={\sum }_{k<p}{u}_k(j),$ the right-hand sum being taken in $(F,+,0_F)$. (Stated here for an arbitrary $X$ because the companion page needs it at $X=\mathbb{N}$.)
2. $e:n\to F^n$ is an ordered basis of $F^n$ (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis); in particular $e$ is injective and its image $e[n]=\{e_i:i<n\}$ is a basis of $F^n$ with $e[n]\approx n$ (Equinumerous sets, $A\approx B$ and $A⪯B$);
3. for every $\lambda :n\to F$ and every $j<n$, $\left({\sum }_{i<n}{\lambda }_i{e}_i\right)(j)={\lambda }_j$; equivalently the coordinate list of $x\in F^n$ with respect to the ordered basis $e$ (A finite list $v:n\to V$ is an ordered basis if and only if every $x\in V$ equals ${\sum }_{i<n}{\lambda }_i{v}_i$ for exactly one $\lambda :n\to F$; those scalars are the coordinates of $x$ in that ordered basis) is $i\mapsto x(i)$;
4. $F^n$ is finite-dimensional over $F$ with ${\dim }_F{F}^n=n$ (Finite-dimensional vector space, and its dimension ${\dim }_{F}V$; infinite-dimensional means having no finite basis);
5. at $n=0$ this reads: $F^0$ has exactly one element, the empty function, so $F^0$ is the zero space, the empty list is its ordered basis, $\mathrm{\varnothing }$ is its basis and ${\dim }_F{F}^0=0$.

Every index runs from $0$, so the coordinates of an element of $F^n$ are $x_0,\dots ,x_{n-1}$ and no statement above is restricted to $n\ge 1$.

• The indices start at $0$ because a natural number is the set of its predecessors. $F^n$ is the function space $F^X$ at $X=n=\{0,\dots ,n-1\}$ (The vector space $F^X$ of all functions $X\to F$ with pointwise operations, and $F^n$ as the case $X=n=\{0,1,\dots ,n-1\}$, On $\mathbb{N}$ the order is membership: $m<n⟺m\in n$), so an element of $F^n$ is a function on $\{0,\dots ,n-1\}$ and there is no $e_n$. Reading the standard basis off a $1$-indexed source would put a vector outside the space at one end and lose one at the other.

• Step 1.1 is not a triviality to be skipped. That a finite sum of functions is the pointwise finite sum is a statement about the recursion defining 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 in two different monoids, and it is proved by induction. Every evaluation argument on this page and on the companion page rests on it.

• This is the concrete counterweight to Every vector space has a basis. Here a basis is written down and no choice principle is used anywhere; there a basis is produced by Zorn's lemma and none is exhibited. The companion page carries both extremes for infinite-dimensional spaces as well: an explicit infinite basis for the eventually zero families, and a basis of $\mathbb{R}$ over $\mathbb{Q}$ that no argument exhibits.