The aim of this paper is to give the detailed proof of the fact that any closed terrez of T of type iAEi represents a provably total function of PA (or HA) from N to N and to get a refinement of this Gödel's theorems part with a careful coding of the Gödel's system T in the Peanos arithmetics. All the notions used here are defined in a previous report: Extension of the definition of the provable totality of a function in the intuitionistic logic HA_pr.