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

証明
x_1, ..., x_n を M-正則列とする。

x_1 による乗法で定義される射: M → M を考える。
x_1 は M-正則だから次の完全列が得られる。

0 → M → M → M/(x_1)M → 0

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

Ext^(p-1)(k, M/(x_1)M) → Ext^p(k, M) → Ext^p(k, M)

M/(x_1)M は長さ n - 1 の正則列をもつから、
帰納法の仮定より、p ≦ n - 1 のとき Ext^(p-1)(k, M/(x_1)M) = 0 である。

即ち、p ≦ n - 1 のとき次の完全列が得られる。

0 → Ext^p(k, M) → Ext^p(k, M)

>>32 より、Ext^p(k, M) → Ext^p(k, M) は x_1 による乗法である。

一方、k は A-加群として、m の元で零化される。特に (x_1)k= 0 である。
よって、>>30 より (x_1)(Ext^p(k, M)) = 0 である。
よって、Ext^p(k, M) = 0 である。
証明終