I am studying the book by Brézis on functional analysis and I just read the open mapping theorem. The proof is split in two steps. Here is a copy of the step 2:
I understood the idea of the proof. My problem is formalizing it. I was trying to deduce the existence of the sequence $(z_n)$, and its properties, possibly using recursion, induction and choice. I just asked a similar question about the Baire theorem and it was suggested to me to apply the axiom of dependent choice (DC).
The theorems I have are
Thm. 1 (Recursion): Let $A$ be a set, $a \in A \ $ and $ \ f:A \to A \ $ be a function. Then there exists an unique sequence $ \ b = (b_n): \mathbb{N} \to A \ $ such that $ \ b_0=a \ $ and $ \ b_{n+1} = f(b_n)$, $\forall n \in \mathbb{N}$.
Thm. 2 (Induction): Let $ \ K \subset \mathbb{N} \ $ be such that $ \ 0 \in K \ $ and, $\forall n \in \mathbb{N}$, if $ \ n \in K$, then $ \ n+1 \in K$. Then $ \ K= \mathbb{N}$.
Together with some version of the axiom of choice or DC. This time I am allowed to use DC.
I tryed to define a relation like that in the answer to my last question but I failed because the (n+1)-th choice depends not only on the n-th choice but on all the previous entries. I need hints to find this relation or to try another approach. Any help is appreciated. Thanks in advance.

If you want to formalize the application of $\sf DC$ in this proof, then you first need to truly understand what $\sf DC$ means, and more specifically, how it is different than just choosing from a countable family of non-empty sets (countable choice).
The main difference is hinted in the name. Dependent Choice. The idea is that each choice you make will be influenced by previous choices, for example, if you have two possible choices for $z_1$, and $\|z_1-z_1'\|>\frac14$, then this means that choosing $z_2$ depends on whether you chose $z_1$ or $z_1'$.
This, in contrast to countable choice, which just tells you to choose without any constraints from a countable family of non-empty sets.
So, back to your question. How do we formalize this? Note that the choice, when applying $\sf DC$, is of the following form: Given a "valid" finite sequence $\langle z_1,\ldots,z_n\rangle$, there is some $z$ such that $\langle z_1,\ldots,z_n,z\rangle$ is also "valid", then there is a function $f\colon\Bbb N\to Z$, such that for every $n$, $f\restriction\{1,\ldots,n\}$ is a "valid" sequence.
(Here "valid" is whatever type of object that you're looking for.)
So all you need to do is argue why when given a sequence of $z_1,\ldots,z_n$ which satisfy the conditions, you can find an extension by some arbitrary vector. Then you can apply $\sf DC$.
If you want to use the axiom of choice in full, which does make this slightly clearer (as it imbues the proof of $\sf DC$ from $\sf AC$), simply fix for every finite "valid" sequence of vectors the set of possible extensions by a single vector, then show these are non-empty, and then fix a choice function.
Now by recursion, choose using this choice function. But instead of considering a function $f\colon E\to E$, here you consider a $A$ to be the set of all finite "valid" sequences, and you consider this choice function as a function from $A$ to itself.