Gale–Shapley: the algorithm produces a stable matching

For every instance $I$ with $n$ men and $n$ women (strict preference lists), the Gale–Shapley (men-proposing deferred acceptance) algorithm is guaranteed to produce a stable matching: there is a bijection $\mu$ from men to women such that, after the algorithm's $n^2$ rounds, every man $m$ is engaged to $\mu(m)$, and $\mu$ has no blocking pair, i.e. there are no $m, w$ with $m$ preferring $w$ to $\mu(m)$ and $w$ preferring $m$ to $\mu^{-1}(w)$.