Proposition 10.2.7 ([I.6.2, SW99]).label 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 10.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 10.2.5, the topology on $E$ is induced by a pseudonorm.$\square$