(⇒) For this portion of the proof we will form the logically-equivalent contrapositive and prove that statement using two cases. “$AB$ is nonsingular implies $A$ and $B$ are both nonsingular” becomes “$A$ or $B$ is singular implies $AB$ is singular.” (Be sure to undertstand why the “and” became an “or”, see Proof Technique CP.)
Case 1. Suppose $B$ is singular. Then there is a nonzero vector $\vect{z}$ that is a solution to $\homosystem{B}$. So \begin{align*} (AB)\vect{z} &=A(B\vect{z})&&\knowl{./knowls/theorem.MMA.knowl}{\text{Theorem MMA}}\\ &=A\zerovector&&\knowl{./knowls/theorem.SLEMM.knowl}{\text{Theorem SLEMM}}\\ &=\zerovector&&\knowl{./knowls/theorem.MMZM.knowl}{\text{Theorem MMZM}}\\ \end{align*}
With Theorem SLEMM we can translate this vector equality to the statement that $\vect{z}$ is a nonzero solution to $\homosystem{AB}$. Thus $AB$ is singular (Definition NM), as desired.
Case 2. Suppose $A$ is singular, and $B$ is not singular. In other words, with Case 1 complete, we can be more precise about this remaining case and assume that $B$ is nonsingular. Because $A$ is singular, there is a nonzero vector $\vect{y}$ that is a solution to $\homosystem{A}$. Now consider the linear system $\linearsystem{B}{\vect{y}}$. Since $B$ is nonsingular, the system has a unique solution (Theorem NMUS), which we will denote as $\vect{w}$. We first claim $\vect{w}$ is not the zero vector either. Assuming the opposite, suppose that $\vect{w}=\zerovector$ (Proof Technique CD). Then \begin{align*} \vect{y} &=B\vect{w}&&\knowl{./knowls/theorem.SLEMM.knowl}{\text{Theorem SLEMM}}\\ &=B\zerovector&&\text{Hypothesis}\\ &=\zerovector&&\knowl{./knowls/theorem.MMZM.knowl}{\text{Theorem MMZM}} \end{align*} contrary to $\vect{y}$ being nonzero. So $\vect{w}\neq\zerovector$. The pieces are in place, so here we go, \begin{align*} (AB)\vect{w} &=A(B\vect{w})&&\knowl{./knowls/theorem.MMA.knowl}{\text{Theorem MMA}}\\ &=A\vect{y}&&\knowl{./knowls/theorem.SLEMM.knowl}{\text{Theorem SLEMM}}\\ &=\zerovector&&\knowl{./knowls/theorem.SLEMM.knowl}{\text{Theorem SLEMM}}\\ \end{align*}
With Theorem SLEMM we can translate this vector equality to the statement that $\vect{w}$ is a nonzero solution to $\homosystem{AB}$. Thus $AB$ is singular (Definition NM), as desired. And this conclusion holds for both cases.
(⇐) Now assume that both $A$ and $B$ are nonsingular. Suppose that $\vect{x}\in\complex{n}$ is a solution to $\homosystem{AB}$. Then \begin{align*} \zerovector &=\left(AB\right)\vect{x}&&\knowl{./knowls/theorem.SLEMM.knowl}{\text{Theorem SLEMM}}\\ &=A\left(B\vect{x}\right)&&\knowl{./knowls/theorem.MMA.knowl}{\text{Theorem MMA}} \end{align*}
By Theorem SLEMM, $B\vect{x}$ is a solution to $\homosystem{A}$, and by the definition of a nonsingular matrix (Definition NM), we conclude that $B\vect{x}=\zerovector$. Now, by an entirely similar argument, the nonsingularity of $B$ forces us to conclude that $\vect{x}=\zerovector$. So the only solution to $\homosystem{AB}$ is the zero vector and we conclude that $AB$ is nonsingular by Definition NM.