Corollary 1

The inequality

holds.

Further, if $K'$ is a finitely generated extension of $K$ and equality holds in (9), then $\Gamma'/\Gamma$ is a finitely generated $\mathbf{Z}$-module and $k'$ is a finitely generated extension of $k$.

Let $r$ and $s$ be natural numbers such that $r \leq r(v'/v)$ and $s \leq s(v'/v)$; we show that $r+s \leq d(K'/K)$ and this will prove (9). By hypothesis there exist elements $x_1, \ldots, x, y_1, \ldots, y$, of $K'$ which satisfy the hypotheses of Theorem 1.

They are therefore algebraically independent over $K$, which shows the inequality $r + s < d(K'/K)$.

If $K'$ is a finitely generated extension of $K$, $d(K'/K)$ is finite, hence $s(v'/v)$ and $r(v'/v)$ are also finite; we denote them by $s$ and $r$. There exist elements $x_1, \ldots, x_s, y_1, \ldots, y_r$ of $K'$ which satisfy the hypotheses of Theorem 1. If $r + s = d(K'/K)$, these elements form a transcendence basis of $K'$ over $K$ and $K'$ is therefore a finite algebraic extension of $K'' = K(x_1, \ldots, y_r)$. Let $\Gamma''$ and $k''$ be the order group and residue field of the restriction of $v'$ to $K''$. By Theorem 1, $\Gamma''/\Gamma$ is a finitely generated $\mathbf{Z}$-module and $k''$ is a finitely generated pure extension of $k$. On the other hand, as $K'$ is a finite algebraic extension of $K$, $\Gamma'/\Gamma$ is a finite group and $k'$ is a finite algebraic extension of $k''$ (§ 8, no. 1, Lemma 2). This proves the corollary.