命題
A を可換環とし、A[[X]] を A 係数の１変数形式的べき級数環とする。
f = a_0 + (a_1)X + (a_2)X^2 + ... を A[[X]] の元とする。
f が A[[X]] の可逆元であるためには a_0 が A の可逆元であることが
必要十分である。

証明
f が A[[X]] の可逆元であれば、fg = 1 となる g ∈ A[[X]] がある。
g = b_0 + (b_1)X + (b_2)X^2 + ... とすれば、
(a_0)(b_0) = 1 である。
よって、a_0 は A の可逆元である。

逆に、a_0 が A の可逆元であるとする。
g = b_0 + (b_1)X + (b_2)X^2 + ... を k[[X]] の元とし、h = fg とおく。
h = c_0 + (c_1)X + (c_2)X^2 + ... とする。

c_0 = (a_0)(b_0)
c_1 = (a_0)(b_1) + (a_1)(b_0)
c_2 = (a_0)(b_2) + (a_1)(b_1) + (a_2)(b_0)
.
.
.
c_n = (a_0)(b_n) + (a_1)(b_(n-1)) + ... + (a_n)(b_0)
.
.
.
である。
a_0 は可逆元であるから、n に関する帰納法より、f と h の係数から
g の係数が定まる。
特に fg = 1 となる g が求まる。
即ち f は 可逆元である。
証明終