diff --git a/src/fa/lc/nuclear-space.tex b/src/fa/lc/nuclear-space.tex
index 6db0791..732492d 100644
--- a/src/fa/lc/nuclear-space.tex
+++ b/src/fa/lc/nuclear-space.tex
@@ -86,4 +86,56 @@
     Let $E$ be a complete nuclear space over $K \in \RC$, then $E$ is a projective limit of Hilbert spaces over $K$. For any Fréchet space $F$, $F$ is nuclear if and only if it is the projective limit of a sequence $\seq{H_n}$ of Hilbert spaces such that the mapping $H_m \to H_n$ is nuclear for all $1 \le m < n < \infty$. 
 \end{corollary}
 
+\begin{proposition}
+\label{proposition:nuclear-subspace}
+    Let $E$ be a nuclear space over $K \in \RC$ and $F \subset E$ be a subspace, then $F$ is also nuclear.
+\end{proposition}
+\begin{proof}
+    Firstly, a setup about auxiliary spaces and subspaces is required. Let $U \in \cn_E(0)$ be convex and circled, then the composition of the inclusion map $\iota: F \to E$ and the canonical projection $\pi_U: E \to E_U$ factors through $F_{U \cap F}$ as follows:  
+    \[
+    \xymatrix{
+    E \ar@{->}[r]^{\pi_U} & E_U \\
+    F \ar@{->}[u]^{\iota} \ar@{->}[r]_{\pi_{U \cap F}} & F_{U \cap F} \ar@{->}[u]_{\widehat \pi_U}
+    }
+    \]
+
+    where $\widehat \pi_U$ is an isometric embedding. As a result, the factored map $\widehat \pi_U: F_{U \cap F} \to E_U$ extends to an isometric embedding on the completions: 
+    \[
+    \xymatrix{
+    E \ar@{->}[r]^{\pi_U} & E_U \ar@{->}[r] & \widehat E_{U} \\
+    F \ar@{->}[u]^{\iota} \ar@{->}[r]_{\pi_{U \cap F}} & F_{U \cap F} \ar@{->}[u]_{\widehat \pi_U} \ar@{->}[r] & \widehat F_{U \cap F} \ar@{->}[u]_{\widehat \pi_U}
+    }
+    \]
+
+    which enables identifying $\widehat F_{U \cap F}$ as a closed subspace of $\widehat E_{U}$.
+
+    To start the proof, let $U \in \cn_E(0)$ be a given convex and circled neighbourhood. Since $E$ is nuclear, there exists a convex and circled neighbourhood $V \in \cn_E(0)$ such that the induced map $\widehat \pi_U: \widehat E_V \to \widehat E_U$ is nuclear. By prior discussion, the following diagram commutes:
+    \[
+    \xymatrix{
+    E \ar@{->}[r]^{\pi_V} & \widehat E_V \ar@{->}[r]^{\widehat \pi_{U}} & \widehat E_U \\
+    F \ar@{->}[u] \ar@{->}[r] & \widehat F_{V \cap F} \ar@{->}[u] \ar@{->}[r]_{\widehat \pi_{U \cap F}} & \widehat F_{U \cap F} \ar@{->}[u]
+    }
+    \]
+
+    Thus the induced map $\widehat \pi_{U \cap F}: \widehat F_{V \cap F} \to \widehat F_{U \cap F}$ corresponds to the restriction of $\widehat \pi_U$ to $\widehat F_{V \cap F}$. Since $\widehat \pi_U$ is nuclear, there exists $\seq{\phi_n} \subset E_V^*$ and $\seq{y_n} \subset \widehat E_U$ such that
+    \[
+    \widehat \pi_U x = \sum_{n = 1}^\infty y_n\dpn{x, \phi_n}{\widehat E_V} \quad \forall x \in \widehat E_V
+    \]
+
+    and $\sum_{n \in \natp} \norm{y_n}_{\widehat E_U}\norm{\phi_n}_{E_V^*} < \infty$. 
+
+    Now, using \autoref{theorem:nuclear-lp}, further assume without loss of generality that $\widehat E_{U}$ is a Hilbert space. Let $P: \widehat E_{U} \to \widehat F_{U \cap F}$ be the orthogonal projection of $\widehat E_U$ onto $\widehat F_{U \cap F}$, then
+    \[
+    \widehat \pi_{U \cap F}x = \sum_{n = 1}^\infty Py_n \dpn{x, \phi_n}{\widehat F_{V \cap F}} \quad \forall x \in \widehat F_{V \cap F}
+    \]
+
+    with
+    \[
+    \normn{\widehat \pi_{U \cap F}}_{N(\widehat F_{V \cap F}; \widehat F_{U \cap F})}
+    \le \sum_{n \in \natp} \norm{Py_n}_{\widehat F_{U \cap F}} \norm{\phi_n}_{F_{V \cap F}^*} \le \sum_{n \in \natp} \norm{y_n}_{\widehat E_U}\norm{\phi_n}_{E_V^*} < \infty
+    \]
+
+    Therefore the induced map $\widehat \pi_{U \cap F}$ is nuclear, and $F$ is a nuclear space.
+\end{proof}
+