Is the closedness of the image of a Fredholm operator implied by the finiteness of the codimension of its image?

Let $X$ and $Y$ be Banach spaces. A bounded operator $T\colon X\to Y$ is called Fredholm iff

• The dimension of $\ker(T)$ is finite,

• The codimension of the image $\mathrm{im}(T)$ is finite,

• The image $\mathrm{im}(T)$ is closed in $Y$.

Question: Is the third condition redundant?

Some lecture notes I'm working through claim that the third condition follows from the second one together with the open mapping theorem. I've checked some books on functional-analysis without finding a proof of this.

Assume that $T$ is injective, because if it is not we know that $\textrm{ker}(T)$ is closed so we can replace $T$ by the induced map from $X/\textrm{ker}(T)$ (which is a Banach space).

Now define $T' := X \oplus C \to Y$ by $T'(x, c) = T(x) + c$ where $C$ is a closed complement for the range of $T$.

This $T'$ is clearly bounded, linear and an isomorphism. So by the open mapping theorem $T'$ is open. Note that $\textrm{im}(T) = T'(X \oplus \{0\})$ which is closed.

The third condition is redundant. The proof I've seen is the following.

Throughout $X,Y$ are Banach spaces and $E$ is a closed subspace of $X$.

Lemma: if $F \subset X$ is finite dimensional then $E+F$ is closed and the image of $E$ in $X/F$ is closed.

proof: reduce to the case $\dim F = 1$, i.e. $F = \mathbb{C} x_0$ with $x_0 \not \in E$ (otherwise $E+F$ is trivially closed). We have to show every convergent subsequence converges to a point in $E + F$. Let $z_n = y_n + c_n x_0$ be such a sequence with limit $z_0$. Let $\delta = dist(x_0, E) > 0$. Now $(z_n)$ is Cauchy so $|z_n - z_m| \to 0$ for $n,m$ sufficiently large. That is, $|(c_n - c_m)x_0 - (y_n -y_m)| \ge |c_n -c_m|\delta \to 0$. It follows that $(c_n)$ is Cauchy so converges to $c_0$. So $y_n$ converges to $z_0 - c_0x_0 \in E$ hence $z_0 \in E + F$ as desired.

So $E+F$ is a Banach space hence so is $E+F/F = Im(E) \in X/F$ which says exactly that its closed in $X/F$. QED

Now we can show $TE$ is closed in $Y$. Let $y_0 + TX, ..., y_n + TX$ be a basis for $Y/TX$ and $Y_0 = span(y_i)$. Consider $T' \colon X \oplus Y_0 \to Y$ given by $T'(x\oplus y) = Tx + y$. This is surjective so $T'' \colon X \oplus Y_0/(\ker T \oplus 0) \to Y$ is invertible. By the lemma $E$ is closed in $X \oplus Y_0/(\ker T \oplus 0)$ and maps to $TE$ under the invertible map $T''$. QED.