In this paper we give a new and comparatively simple proof of the following theorem by Girard [1]:“If ∀x∈ ${\cal O}$ ∃y∈ ${\cal O}$ ψ(x,y) (where the relationψ is arithmetic and positive in Kleene's ${\cal O}$ ), then there exists a recursive DilatorD such that ∀α≧ω∀x∈ ${\cal O}$ <α∃y∈ ${\cal O}$ (...) modification of Girard's system in [1]) we construct in a uniform way for each ordinalα a derivation Tα of the formula ∀x ∈ ${\cal O}$ <α∃y∈ ${\cal O}$ ψ(x, y), and then defineD immediately from the family (Tα)α∈On. Especially we set D(α):=Kleene-Brouwer length of (Tα). (shrink)