Proof of Theorem EMNS

The conclusion of this theorem is an equality of sets, so normally we would follow the advice of Definition SE. However, in this case we can construct a sequence of equivalences which will together provide the two subset inclusions we need. First, notice that $\zerovector\in\eigenspace{A}{\lambda}$ by Definition EM and $\zerovector\in\nsp{A-\lambda I_n}$ by Theorem HSC. Now consider any nonzero vector $\vect{x}\in\complex{n}$, \begin{align*} \vect{x}\in\eigenspace{A}{\lambda}&\iff A\vect{x}=\lambda\vect{x}&&\knowl{./knowls/definition.EM.knowl}{\text{Definition EM}}\\ &\iff A\vect{x}-\lambda\vect{x}=\zerovector&&\knowl{./knowls/property.AIC.knowl}{\text{Property AIC}}\\ &\iff A\vect{x}-\lambda I_n\vect{x}=\zerovector&&\knowl{./knowls/theorem.MMIM.knowl}{\text{Theorem MMIM}}\\ &\iff\left(A-\lambda I_n\right)\vect{x}=\zerovector&&\knowl{./knowls/theorem.MMDAA.knowl}{\text{Theorem MMDAA}}\\ &\iff\vect{x}\in\nsp{A-\lambda I_n}&&\knowl{./knowls/definition.NSM.knowl}{\text{Definition NSM}} \end{align*}