I found a reference in Kaup/Kaup, a proof of the theorem is given in Appendix B (Theorem 12) of
Gunning, R.C., Rossi, H.: Analytic Functions of Several Complex Variables. Englewood Cliffs, N. J.: Prentice-Hall 1965.
I don't like that proof very much, though, the mixture of which definitions and facts are assumed to be known and which are explicitly stated doesn't resonate with my mathematical upbringing.
In the following, I will present (a variation of) a proof given in a lecture by Ingo Lieb on Stein manifolds I heard a couple of decades ago. The proof is a little ad-hoc, but very explicit and elementary. Some basic knowledge about topological vector spaces is assumed of course.
Lemma: Let $\varphi \colon E \to F$ a surjective continuous linear map between Fréchet spaces (or just complete metrisable spaces, local convexity isn't needed here). For every compact $L \subset F$ there is a compact $K \subset E$ with $\varphi(K) = L$.
Proof: Let $V_0 \supset V_1 \supset V_2 \supset \dotsc$ a neighbourhood basis of $0$ in $E$ such that all $V_n$ are balanced, and $V_{n+1} + V_{n+1} \subset V_n$ for all $n$. Put $U_n = \varphi(V_n)$ for $n\in \mathbb{N}$. By the open mapping theorem $\{U_n : n \in \mathbb{N}\}$ is a neighbourhood basis of $0$ in $F$.
Since $L$ is compact, for every $n$ there is a finite subset $T_n \subset L$ with $L \subset T_n + U_n$. Let $S_0 \subset E$ a set that is mapped bijectively to $T_0$ by $\varphi$. Having found $S_0, \dotsc, S_m$, we construct $S_{m+1}$ as follows: For every $t \in T_{m+1}$ choose a $t' \in T_m$ with $t - t' \in U_{m+1}$. Let $s'$ be that element of $S_m$ with $\varphi(s') = t'$. Choose $s \in s' + V_{m+1}$ with $\varphi(s) = t$ - that is possible since $\varphi(s' + V_{m+1}) = \varphi(s') + \varphi(V_{m+1}) = t' + U_{m+1} \ni t$ and let $S_{m+1}$ be the set of all thus chosen $s$. So $S_{m+1}$ is a finite set that is mapped bijectively to $T_{m+1}$ by $\varphi$, and $S_{m+1} \subset S_m + V_{m+1}$. Define $T = \bigcup_n T_n$ and $S = \bigcup_n S_n$. Then $T$ is a dense subset of $L$ and $\varphi(S) = T$. Furthermore, $S$ is precompact (totally bounded): given a neighbourhood $V$ of $0$, choose $n$ such that $V_n \subset V$. Let $A = \bigcup_{k = 0}^n S_k$. Then $A$ is a finite set, and $S \subset A + V_n \subset A + V$. For, if $s \in S \setminus A$ there is an $r > n$ with $s \in S_r$. By construction, there is an $s_{r-1} \in S_{r-1}$ with $s - s_{r-1} \in V_r$, an $s_{r-2} \in S_{r-2}$ with $s_{r-1} - s_{r-2} \in V_{r-1}$, …, and finally an $s_n \in S_n$ with $s_{n+1} - s_n \in V_{n+1}$. Then
$$s - s_n \in V_r + V_{r-1} + \dotsc + V_{n+1} \subset V_n\,,$$
i.e. $s \in s_n + V_n \subset A + V_n$. By completeness of $E$, $K := \overline{S}$ is compact, hence $\varphi(K)$ is closed, and
$$T = \varphi(S) \subset \varphi(K) = \varphi(\overline{S}) \subset \overline{\varphi(S)} = \overline{T} = L$$
shows $\varphi(K) = L$ as desired. We note that if $L$ is symmetric ($L = -L$) or balanced, then $K$ can be chosen to be symmetric or balanced respectively.
Proof of the Theorem: Let $U$ a balanced neighbourhood of $0$ in $E$ such that $\psi(U)$ is relatively compact, define $L = \overline{\psi(U)}$ and find a balanced compact $K$ with $\varphi(K) = L$. By compactness, there is a finite $S = \{y_1, \dotsc, y_s\} \subset K$ with $K \subset S + \frac{1}{2}U$. For $1 \leqslant i \leqslant s$, let $x_i = \varphi(y_i)$. We will show
$$F = \operatorname{Im} (\varphi - \psi) + \operatorname{span}\:\{ x_1, \dotsc, x_s\}\,.\tag{1}$$
First we consider $y \in K$. We construct two sequences $(\eta_n)$ in $K$ and $(\zeta_n)$ in $S$ such that always $$\eta_n \in \zeta_n + \frac{1}{2}U.\tag{$\ast$}$$ We set $\eta_0 = y$, and choose $\zeta_0$ such that $(\ast)$ holds. If $\eta_n$ and $\zeta_n$ are found for $n \leqslant m$, by $(\ast)$ we have $2(\eta_m - \zeta_m) \in U$, whence $\psi(2(\eta_m - \zeta_m)) \in L = \varphi(K)$ and we choose $\eta_{m+1} \in K$ with $\varphi(\eta_{m+1}) = 2\psi(\eta_m - \zeta_m)$. Then we choose $\zeta_{m+1}\in S$ such that $(\ast)$ holds.
So for every $m$ we have
$$\varphi(\eta_m) - \varphi(2^{-1}\eta_{m+1}) = \varphi(\eta_m) - \psi(\eta_m - \zeta_m) = (\varphi - \psi)(\eta_m) - (\varphi - \psi)(\zeta_m) + \varphi(\zeta_m)\,.\tag{2}$$
Since $K$ is compact, the series $\sum 2^{-m}\eta_m$ and $\sum 2^{-m} \zeta_m$ are convergent, and there are $\alpha_1, \dotsc, \alpha_s \in \mathbb{R}$ with
$$\sum_{m = 0}^{\infty} 2^{-m}\zeta_m = \sum_{i = 1}^s \alpha_i y_i\,.$$
Using telescoping and $(2)$ we obtain
\begin{align}
\varphi(y) &= \varphi\Biggl(\sum_{m = 0}^{\infty} \bigl(2^{-m}\eta_m - 2^{-m-1}\eta_{m+1}\bigr)\Biggr) \\
&= \sum_{m = 0}^{\infty} \varphi\bigl(2^{-m}\eta_m - 2^{-m-1}\eta_{m+1}\bigr) \\
&= \sum_{m = 0}^{\infty} \Bigl((\varphi - \psi)\bigl(2^{-m}\eta_m - 2^{-m}\zeta_m\bigr) + \varphi\bigl(2^{-m}\zeta_m\bigr)\Bigr) \\
&= (\varphi - \psi)\Biggl(\sum_{m = 0}^{\infty} 2^{-m}(\eta_m - \zeta_m)\Biggr) + \varphi\Biggl(\sum_{m = 0}^{\infty} 2^{-m}\zeta_m\Biggr) \\
&= (\varphi - \psi)(\hat{y}) + \sum_{i = 1}^s \alpha_i x_i\,.
\end{align}
Next we consider an arbitrary $y \in E$. Since $U$ is a neighbourhood of $0$, there is a $\lambda > 0$ with $\lambda y \in U$. Then $\psi(\lambda y) \in L$, so there is $y' \in K$ with $\varphi(y') = \psi(\lambda y)$. Thus
\begin{align}
\varphi(y) &= \lambda^{-1} \varphi(\lambda y) \\
&= \lambda^{-1}\bigl[(\varphi - \psi)(\lambda y) + \psi(\lambda y)\bigr] \\
&= \lambda^{-1}\bigl[(\varphi - \psi)(\lambda y) + \varphi(y')\bigr] \\
&= \lambda^{-1}\Biggl[(\varphi - \psi)(\lambda y) + (\varphi - \psi)(y'') + \sum_{i = 1}^s \alpha_i x_i\Biggr] \\
&= (\varphi - \psi)\bigl(y + \lambda^{-1}y''\bigr) + \sum_{i = 1}^s \bigl(\lambda^{-1}\alpha_i\bigr)x_i\,.
\end{align}
Since $\varphi$ is surjective, the proof of $(1)$ is complete. Additionally, as a consequence of the open mapping theorem, if the image of a continuous linear map between Fréchet spaces has finite codimension, then it is closed, so $\operatorname{Im}(\varphi - \psi)$ is closed.
I like Laurent Schwartz's original proof very much, it is concise and transparent. But it of course assumes quite a bit of duality theory of Hausdorff locally convex spaces.
Laurent Schwartz's proof: (C. R. Acad. Sci. Paris, 236 (1953), p. 2472-2473; translation by me)
All spaces are assumed to be Hausdorff locally convex topological vector spaces over $\mathbb{R}$ or $\mathbb{C}$.
Theorem 1: Let $u, v \colon E \to F$ be continuous linear maps, and suppose that $u$ is an isomorphism to $u(E)$, which is closed, and $v$ is compact. Then $w = u + v$ is a homomorphism, its kernel $N$ has finite dimension, and $w(E)$ is closed.
Note: That $u$ is an isomorphism to $u(E)$ means $u$ is injective, and its inverse $u^{-1} \colon u(E) \to E$ is also continuous. Naturally, $u(E)$ is endowed with the subspace topology induced from $F$. That $w$ is a homomorphism means that the induced map $\overline{w} \colon E/N \to w(E)$ is an isomorphism in the sense elaborated before.
Proof: By compactness of $v$, there is a continuous seminorm $p$ on $E$ such that the closed $p$-unit ball $V = \{ x \in E : p(x) \leqslant 1\}$ has relatively compact image $v(V)$. Let $W = V \cap N$. Then $u(W) = -v(W)$ is precompact. Since $u$ is an isomorphism, it follows that $W$ is precompact, whence $N$ is finite-dimensional. Restricting $u$ and $v$ to a topological complement of $N$ reduces to the case $N = \{0\}$. Assume hence that $w$ is injective. Let $\mathscr{U}$ be an ultrafilter on $E$ such that $w(\mathscr{U})$ converges in $F$. The proof will be completed by showing that $\mathscr{U}$ converges.
Let $a \in [0,+\infty]$ the limit of $p(\mathscr{U})$. Consider first the case $a < +\infty$. Then $(a+1)V \in \mathscr{U}$, and therefore $v(\mathscr{U})$ converges in $F$. Thus $u(\mathscr{U})$ also converges in $F$. Since $u(E)$ is closed and $u$ is an isomorphism, it follows that $\mathscr{U}$ converges in $E$.
Finally, we show that $a = +\infty$ is impossible. Otherwise, $w[x/p(x)]$ would converge to $0$ along $\mathscr{U}$, and $v[x/p(x)]$ would have a limit; hence $u[x/p(x)]$ would also have a limit, and therefore $x/p(x)$ too. Call the latter $y_0$. One would then have $p(y_0) = 1$ and $w(y_0) = 0$, contradicting the injectivity of $w$.
Theorem 2: Let $u, v \colon E \to F$ continuous linear maps. Suppose that $u$ is a surjective weak homomorphism [that is, a homomorphism if we endow $E$ and $F$ with their respective weak topologies] and $v$ compact, and that $u$ has the property
$(K)$ Every convex compact subset of $F$ is contained in the image of a convex compact subset of $E$ under $u$.
Then $w = u+v$ is a weak homomorphism from $E$ onto a closed subspace of $F$ with finite codimension.
Proof: We endow the duals $E'$ and $F'$ respectively with the topology $\tau_c$ of uniform convergence on convex compact subsets of $E$ and $F$ repsectively. Since $v(V)$ is relatively compact [for a suitable neighbourhod $V$ of $0$], the transpose ${}^tv$ maps the polar of $v(V)$ to an equicontinuous, hence relatively compact, subset of $E'$. It follows that ${}^tv$ is compact. By the hypothesis $(K)$, the convergence of $z' \in F'$ to $0$ is equivalent to the convergence of ${}^tu(z')$ to $0$ in $E'$. Therefore ${}^tu$ is an isomorphism from $F'$ to ${}^tu(F')$. Now, $u$ being a weak homomorphism, ${}^tu(F')$ is weakly closed in $E'$, hence closed with respect to $\tau_c$.
Thus ${}^tu$ and ${}^tv$ satisfy the hypotheses of Theorem 1. Therefore:
- ${}^tw(F')$ is closed with respect to $\tau_c$. But $\tau_c$ lies between $\sigma(E',E)$ and $\tau(E',E)$, hence ${}^tw(F')$ is also weakly closed, which proves that $w$ is a weak homomorphism.
- ${}^tw$ is a homomorphism with respect to the topologies $\tau_c$; with respect to these topologies the duals of $E'$ and $F'$ are $E$ and $F$ respectively by the reasoning in 1. Therefore ${}^tw$ is a homomorphism for $\sigma(F',F)$ and $\sigma(E',E)$, and $w(E)$ is closed.
- The kernel of ${}^tw$ has finite dimension, hence the image of $w$, which is closed, has finite codimension.
Corollary of Theorem 2: Let $E,F$ be two Fréchet spaces, $u \colon E \to F$ a continuous linear surjection, $v \colon E \to F$ linear and compact. Then $w = u + v$ maps $E$ to a closed subspace of $F$ with finite codimension.
Proof: By the open mapping theorem, $u$ is a homomorphism, hence a fortiori a weak homomorphism. Further one easily verifies that $u$ satisfies condition $(K)$ [see the lemma above].
