命題
A をネーター局所環とし、m をその極大イデアル、
M ≠ 0 を有限生成 A-加群とする。
k = A/m とおく。
n > 0 を整数とし、0 ≦ i ≦ n - 1 のとき Ext^i(k, M) = 0
であれば、長さ(>>28) n の M-正則列が存在する。

証明
n に関する帰納法を使う。
Ext^0(k, M) = Hom(k, M) だから、n = 1 のときは、
>>26 で証明されている。

よって n ≧ 2 と仮定する。
Hom(k, M) = 0 だから、>>26 より x ∈ m で M-正則なものがある。
x による乗法で定義される射: M → M を考える。
x は M-正則だから次の完全列が得られる。

0 → M → M → M/xM → 0

これから次の完全列が得られる。

Ext^i(k, M) → Ext^i(k, M/xM) → Ext^(i+1)(k, M)

ここで、i は任意の整数 i ≧ 0 である。
仮定より、0 ≦ i ≦ n - 1 のとき Ext^i(k, M) = 0 だから、
0 ≦ i ≦ n - 2 のとき Ext^i(k, M/xM) = 0 である。

帰納法の仮定を M/xM に適用すれば、長さ n - 1 の (M/xM)-正則列
x_2, ..., x_n が存在する。
よって、x, x_2, ..., x_n は M-正則列となり、長さは n である。
証明終