  Hilbert's epsilon calculus is an extension of elementary or predicate
calculus by a term-forming operator $\varepsilon$ and initial formulas
involving such terms. The fundamental results about the epsilon calculus are
so-called epsilon theorems, which have been proven by means of the epsilon
elimination method. It is a procedure of transforming a proof in epsilon
calculus into a proof in elementary or predicate calculus through getting rid
of those initial formulas. One remarkable consequence is a proof of Herbrand's
theorem due to Bernays and Hilbert which comes as a corollary of extended first
epsilon theorem. The contribution of this paper is the upper and lower bounds
analysis of the length of Herbrand disjunctions in extended first epsilon
theorem for epsilon calculus with equality. We also show that the complexity
analysis for Herbrand's theorem with equality is a straightforward consequence
of the one for extended first epsilon theorem without equality due to Moser and
Zach.
