I'm trying to prove this well-known result. Could you have a check on my attempt?
Let $(E, | \cdot|)$ be a normed linear space and $E^\star$ its continuous dual space. If $E$ is finite-dimensional, then $\dim E =\dim E^\star$.
My proof: Assume $\{e_1, \ldots, e_n\}$ is a basis of $E$. For $k \in \{1, \ldots, n\}$, we define $f_k : E \to \mathbb R$ that sends $x$ to its $k$-th coordinate, i.e., $$f_k \left ( \sum_{m=1}^n \lambda_m e_m \right ) := \lambda_k.$$ It's clear that $f_1 \ldots, f_n \in E^\star$. Take $\alpha_1, \ldots, \alpha_n \in \mathbb R$ such that $\sum_{k=1}^n \alpha_k f_k =0_{E^\star}$. We pick a particular $\overline x := \sum_{m=1}^n \alpha_m e_m$. Then $\sum_{k=1}^n \alpha_k f_k(\overline x) =0$ implies $\sum_{k=1}^n \alpha^2_k = 0$ and thus $\alpha_1 = \cdots = \alpha_n=0$. It follows that $\{f_1 \ldots, f_n\}$ is linearly independent. Notice that $$\bigcap_{k=1}^n \ker f_k = \{0_E\} \subseteq \ker f, \quad \forall f\in E^\star.$$
Lemma: Let $f_1, \ldots,f_n,f$ be linear functionals such that $\bigcap_{k=1}^n \ker f_k \subseteq \ker f$. Then $f$ is linearly dependent from $f_1,\ldots,f_n$.
By our lemma, each $f\in E^\star$ is linearly dependent of $f_1, \ldots, f_n$. Hence $\{f_1 \ldots, f_n\}$ is indeed a basis of $E^\star$. This completes the proof.
Best Answer
Your argument is fine. Just a couple comments.
The basis you constructed is the dual basis of $e_1,\ldots,e_n$. The linear independence can be obtained in a marginally easier way if you just evaluate on each $e_k$, since $\Big(\sum_j\alpha_jf_j\Big)(e_k)=\alpha_k$.
Like Theo I love the Lemma, but it is a bit overkill here. You could just note directly, by evaluating on an $x$, that $$ f=\sum_jf(e_j)\,f_j. $$