A result on separable Fréchet spaces In the proof of the following theorem:
if $X$ is a separable Fréchet space, then $\mathcal{E}(X)=\mathcal{B}(X)$.
Where $\mathcal{E}(X)$ is the $\sigma$-algebra generated by the cylindrical sets on $X$ and $\mathcal{B}(X)$ is the Borel $\sigma$-algebra.
They start by taking $(x_n)$ a dense sequence in $X$, and a family of seminorms $(p_k)$  which defines the topology of $X$. The part of the proof that I didn't get is the following:
By the Hahn-Banach theorem for every $n$ and $k$ there is $l_{n,k}\in X^*$ such that $p_k(x_n)=l_{n,k}(x_n)$ and $\sup\{l_{n,k}(x):\ p_k(x)\leq 1\}=1$. As a consequence, for every $x\in X$ and $k\in\mathbb{N}$ we have $p_k(x)=\sup_n\{l_{n,k}(x)\}$.
Questions:
*on which linear application did they apply the Hahn-Banach theorem ? 
*what did they use to obtain $p_k(x)=\sup_n\{l_{n,k}(x)\}$ as a consequence ?
Thank you for your time.
 A: Define a linear functional $l_{n,k}(\alpha x_n) = \alpha p_k(x_n)$ on the line through $x_n$. Check that $l_{n,k}(\alpha x_n) \le p_k(\alpha x_n)$ for all $\alpha$.
Now extend $l_{n,k}$ to all of $X$ using Hahn Banach such that
$l_{n,k}(x) \le p_k(x)$ for all $x$.
Now suppose $p_k(x) \le 1$, then we have $l_{n,k}(x) \le 1$. Furthermore,
we have $l_{n,k}({1 \over p_k(x_n)} x_n) = {1 \over p_k(x_n)} p_k(x_n) = 1$,
and so $\sup_{p_k(x) \le 1} l_{n,k}(x) = 1$.
For the last part, note that
$l_{n,k}(x) \le p_k(x)$ for all $x$ and hence 
$\sup_n l_{n,k}(x) \le p_k(x)$ for all $x$. So, all that remains is to show equality.
Fix $x$ and note that
$l_{n,k}(y) = l_{n,k}(x) + l_{n,k}(y-x) \le l_{n,k}(x) + p_k(y-x)$, or
$l_{n,k}(y) -p_k(y-x) \le l_{n,k}(x)$.
Since $x_n$ is dense, there is some subsequence $x_{n_i} \to x$, so replacing $n$ by $n_i$ and $y$ by $x_{n_i}$ we get
$l_{n_i,k}(x_{n_i}) -p_k(x_{n_i}-x) = p_k(x_{n_i})-p_k(x_{n_i}-x) \le l_{n_i,k}(x) \le \sup_n l_{n,k}(x) $
Since $p_k(x_{n_i}) \to p_k(x)$, $p_k(x_{n_i}-x) \to 0$, we get
$p_k(x) \le \sup_n l_{n,k}(x) $.
