Proof of Theorem OSIS

The matrix $I_n$ is nonsingular (since it row-reduces easily to $I_n$, Theorem NMRRI). So $A$ and $B$ are nonsingular by Theorem NPNT, so in particular $B$ is nonsingular. We can therefore apply Theorem CINM to assert the existence of a matrix $C$ so that $BC=I_n$. This application of Theorem CINM could be a bit confusing, mostly because of the names of the matrices involved. $B$ is nonsingular, so there must be a “right-inverse” for $B$, and we are calling it $C$.

Now \begin{align*} BA &=(BA)I_n&&\knowl{./knowls/theorem.MMIM.knowl}{\text{Theorem MMIM}}\\ &=(BA)(BC)&&\knowl{./knowls/theorem.CINM.knowl}{\text{Theorem CINM}}\\ &=B(AB)C&&\knowl{./knowls/theorem.MMA.knowl}{\text{Theorem MMA}}\\ &=BI_nC&&\text{Hypothesis}\\ &=BC&&\knowl{./knowls/theorem.MMIM.knowl}{\text{Theorem MMIM}}\\ &=I_n&&\knowl{./knowls/theorem.CINM.knowl}{\text{Theorem CINM}} \end{align*} which is the desired conclusion.