The standard list $e : n \to F^{n}$ with $e_i(i) = 1_F$ and $e_i(j) = 0_F$ for $j \ne i$ is an ordered basis of $F^{n}$; hence $\dim_F F^{n} = n$, and $F^{0}$ is the zero space with basis $\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 \iff m \in n$). For $i < n$ define the standard unit vector $e_i \in F^{n}$ by

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

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$, $\Bigl(\sum_{k<p} u_k\Bigr)(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 \preceq B$);
3. for every $\lambda : n \to F$ and every $j < n$, $\bigl(\sum_{i<n}\lambda_i e_i\bigr)(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, $\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 \iff 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.