[proofplan] We prove the stronger coordinate statement: the canonical bidual map sends each basis vector $e_i$ to the functional on $V^*$ that extracts the $i$-th dual-basis coordinate. This is exactly the defining property of the [dual basis](/theorems/414) to $(e_1^*,\ldots,e_n^*)$. Once the images of the basis $\mathcal B$ are identified with a basis of $V^{**}$, the map $\iota_V$ is an isomorphism because it sends a basis of $V$ to a basis of $V^{**}$. The zero-dimensional case is included by interpreting all displayed ordered bases as empty ordered bases. [/proofplan] [step:Check that the canonical bidual map is linear] Let $V^*=\operatorname{Hom}_k(V,k)$ and $V^{**}=\operatorname{Hom}_k(V^*,k)$. For each $v\in V$, the element $\iota_V(v)\in V^{**}$ is the map \begin{align*} \iota_V(v): V^* \to k,\quad \varphi \mapsto \varphi(v). \end{align*} First, $\iota_V(v)$ is $k$-linear in $\varphi$: for $\varphi,\psi\in V^*$ and $a,b\in k$, \begin{align*} \iota_V(v)(a\varphi+b\psi)=(a\varphi+b\psi)(v)=a\varphi(v)+b\psi(v)=a\iota_V(v)(\varphi)+b\iota_V(v)(\psi). \end{align*} Thus $\iota_V(v)\in V^{**}$. Now let $v,w\in V$ and $a,b\in k$. For every $\varphi\in V^*$, \begin{align*} \iota_V(av+bw)(\varphi)=\varphi(av+bw)=a\varphi(v)+b\varphi(w)=(a\iota_V(v)+b\iota_V(w))(\varphi). \end{align*} Since two elements of $V^{**}$ are equal exactly when they agree on every $\varphi\in V^*$, this gives \begin{align*} \iota_V(av+bw)=a\iota_V(v)+b\iota_V(w). \end{align*} Therefore $\iota_V:V\to V^{**}$ is $k$-linear. [/step] [step:Compute the bidual images on the dual basis] Let $\delta_{ij}\in k$ denote the Kronecker delta, so $\delta_{ij}=1$ if $i=j$ and $\delta_{ij}=0$ if $i\ne j$. Since $\mathcal B^*=(e_1^*,\ldots,e_n^*)$ is the dual basis to $\mathcal B=(e_1,\ldots,e_n)$, we have \begin{align*} e_j^*(e_i)=\delta_{ij} \end{align*} for all $1\le i,j\le n$. For each $1\le i\le n$, evaluate $\iota_V(e_i)\in V^{**}$ on the basis vector $e_j^*\in V^*$. By the definition of $\iota_V$, \begin{align*} \iota_V(e_i)(e_j^*)=e_j^*(e_i)=\delta_{ij}. \end{align*} Thus $\iota_V(e_i)$ is the functional on $V^*$ that takes value $1$ on $e_i^*$ and value $0$ on every $e_j^*$ with $j\ne i$. [guided] The object $\iota_V(e_i)$ lives in $V^{**}$, so it is a linear functional on $V^*$. To identify it, it is enough to know its values on the basis $\mathcal B^*=(e_1^*,\ldots,e_n^*)$ of $V^*$. The defining rule for the canonical bidual map says that $\iota_V(e_i)$ evaluates a functional at the vector $e_i$: \begin{align*} \iota_V(e_i)(\varphi)=\varphi(e_i) \end{align*} for every $\varphi\in V^*$. We now apply this rule to the particular functional $\varphi=e_j^*$. Since $\mathcal B^*$ is the dual basis to $\mathcal B$, the defining dual-basis relation is \begin{align*} e_j^*(e_i)=\delta_{ij}. \end{align*} Therefore \begin{align*} \iota_V(e_i)(e_j^*)=e_j^*(e_i)=\delta_{ij}. \end{align*} This computation is exactly the dual-basis test inside $V^{**}$: a functional on $V^*$ is the $i$-th dual functional to the ordered basis $\mathcal B^*$ precisely when it sends $e_i^*$ to $1$ and sends every other $e_j^*$ to $0$. [/guided] [/step] [step:Identify the dual basis of $\mathcal B^*$ in $V^{**}$] Let $(\varepsilon_1,\ldots,\varepsilon_n)$ denote the dual basis of the ordered basis $\mathcal B^*=(e_1^*,\ldots,e_n^*)$ of $V^*$. Thus each $\varepsilon_i\in V^{**}$ is characterized by \begin{align*} \varepsilon_i(e_j^*)=\delta_{ij} \end{align*} for all $1\le i,j\le n$. The computation above gives the same defining relation for $\iota_V(e_i)$: \begin{align*} \iota_V(e_i)(e_j^*)=\delta_{ij}. \end{align*} Since a linear functional on $V^*$ is uniquely determined by its values on the basis $\mathcal B^*$, we obtain \begin{align*} \iota_V(e_i)=\varepsilon_i \end{align*} for each $1\le i\le n$. Hence the dual basis of $\mathcal B^*$ in $V^{**}$ is \begin{align*} (\iota_V(e_1),\ldots,\iota_V(e_n)). \end{align*} [/step] [step:Conclude that $\iota_V$ is an isomorphism] Choose an ordered basis $\mathcal B=(e_1,\ldots,e_n)$ of $V$. The tuple $(\iota_V(e_1),\ldots,\iota_V(e_n))$ is the dual basis of $\mathcal B^*$, hence is a basis of $V^{**}$. Since $\mathcal B=(e_1,\ldots,e_n)$ is a basis of $V$ and the $k$-[linear map](/page/Linear%20Map) $\iota_V$ sends this basis to a basis of $V^{**}$, $\iota_V$ is bijective and therefore a $k$-linear isomorphism. If $n=0$, then $V=\{0\}$, $V^*=\{0\}$, and $V^{**}=\{0\}$. The same argument reads with empty ordered bases: the empty tuple is the dual basis of the empty tuple, and the unique map $\{0\}\to\{0\}$ is an isomorphism. This completes the proof. [/step]