Proposition 8.2.9. Let $E$ be a locally bounded TVS over $K \in \RC$, then there exists a pseudonorm $\rho: E \to [0, \infty)$ that induces the topology on $E$.
Proof. Let $U \in \cn^{o}(0)$ be bounded. Using Proposition 8.1.11, assume without loss of generality that $U$ is circled. For each $n \in \natp$, let $U_{n} = n^{-1}U$. Let $V \in \cn^{o}(0)$, then there exists $\lambda \in K$ such that $\lambda V \supset U$, $\abs{\lambda}^{-1}U \subset V$. For any $n \in \natp$ with $n^{-1}< \abs{\lambda}^{-1}$, $U_{n} \subset V$. Thus $E$ admits a countable fundamental system of neighbourhoods at $0$. By Theorem 8.2.6, the topology on $E$ is induced by a pseudonorm.$\square$