命題
F を可換体とし、F((X)) を F 係数の１変数形式的べき級数体(>>57)とする。
F((X)) は >>72の位相で完備である。

証明
g = (a_p)X^p + (a_(p+1)X^(p+1) + ... を F((X)) の元としたとき、
g の n 次以下の項の和
(a_p)X^p + (a_(p+1)X^(p+1) + ... + (a_n)X^n を [g]_n と書くことにする。
n ＜ p のときは [g]_n = 0 とする。

(f_n), n = 1, 2, ... を F((X)) における Cauchy 列とする。
任意の整数 n ＞ 0 に対して 整数 m(n) ＞ 0 が定まり、
i, j ≧ m(n) のとき ord(f_i - f_j) ≧ n + 1 となる。
このとき、[f_i]_n = [f_j]_n である。
i = m(n) のときの [f_i]_n を g_n とする。
k ＞ n のとき [g_k]_n = g_n である。
よって、F((X)) の元 g で任意の整数 n ＞ 0 に対して [g]_n = g_n となる
ものが一意に存在する。
i ≧ m(n) のとき [g]_n = [f_i]_n であるから ord(f_i - g) ≧ n + 1 となる。
よって、i → +∞ のとき、lim f_i = g である。
証明終