Solution (source code)

= Solution

The open mapping lemma says: if a bounded <linear map> between Banach spaces satisfies $\overline{T(B_X)}\supset rB_Y$, then $T(B_X)$ contains a (possibly smaller) ball. Given $y$, repeatedly choose corrections $x_n$ whose residuals shrink geometrically; completeness makes $\sum x_n$ converge and maps it to $y$. Baire category applied to $Y=\bigcup_nT(nB_X)$ supplies the closure hypothesis for a surjective map. This proves the <Open mapping theorem (functional analysis)>.