Proposition 13

If E is a free module (resp. a free module with a finite basis), the canonical mapping $c_E : E \to E^{**}$ is injective (resp. bijective).

Let $(e_t)_{t \in T}$ be a basis of E and let $(e_t^*)$ be the family of corresponding coordinate forms; by definition, if $x \in E$ is such that $\tilde{x} = 0$, then $\langle x, e_t^* \rangle = 0$ for all $t \in T$, in other words all the coordinates of $x$ are zero, hence $x = 0$. Suppose further that T is finite; since $\langle \tilde{e}_t, e_{t'}^* \rangle = \delta_{tt'}$, $(\tilde{e}_t)$ is the dual basis of $(e_t^*)$ in $E^{**}$ and, as $c_E$ transforms a basis of E into a basis of $E^{**}$, $c_E$ is bijective (§ 1, no. 11, Corollary 3 to Proposition 17). We have moreover proved: