Internal direct product theorem

If $H,K⊴G$, $H\cap K=\{1\}$, and $HK=G$, then multiplication defines an isomorphism $H\times K\to G$. Conversely, the two canonical factors of a direct product satisfy these conditions.