命題
A をネーター環とし、I をそのイデアル、
M を有限生成 A-加群で、M ≠ IM とする。
このとき depth(I, M) は有限である。
さらに depth(I, M) ≦ inf {dim(M_p); p ∈ Supp(M/IM)} である。

証明
M ≠ IM だから Supp(M/IM) は空でない。
p を Supp(M/IM) に属する任意の素イデアルとする。
前スレ2の>>953 より Supp(M/IM) = V(I) ∩ Supp(M) である。
φ: A → A_p を標準射とする。

x_1, ..., x_r を I に含まれる M-正則列 とする。
I ⊂ p だから φ(x_1), ..., φ(x_r) は pA_p に含まれる。
さらに p ∈ Supp(M) だから M_p ≠ 0 である。
>>53 より、φ(x_1), ..., φ(x_r) は M_p に関しての
正則列である。よって、>>34 より r ≦ dim(M_p) である。
よって、I に含まれ x_1, ..., x_r を含む M-正則列で極大
なものが存在する。その長さを s とする。
depth(I, M) > s とすると >>52 より I に含まれる M-正則列で
長さ s + 1 のものが存在する。これは s の取り方に反する。
よって、depth(I, M) ≦ s である。
さらに s ≦ dim(M_p) だから depth(I, M) ≦ dim(M_p) である。
証明終