Corollary

The dimension of $M$ is the smallest of the integers $d \geqslant 0$ for which there exists a sequence $(x_1, ..., x_d)$ of elements of $m_A$ such that the $A$-module $M / \sum_{i=1}^d x_i M$ is of finite length.

Since $\varnothing$ is a secant subset for $M$, Theorem 1, b) proves the existence of a maximal secant sequence for $M$, say $(x_1, ..., x_d)$. But then one has $d = \dim_A(M)$ and the $A$-module $M / \sum_{i=1}^d x_i M$ is of finite length by property (iii) of Theorem 1, c). Conversely, if $(x'_1, ..., x'_{d'})$ is a sequence of elements of $m_A$ such that the $A$-module $M / \sum_{j=1}^{d'} x'_j M$ is of finite length, one has $d' \geqslant \dim_A(M)$ by Theorem 1, a).

Recall (III, § 3, No. 2, Definition 1) that an ideal $q$ of a noetherian local ring $A$ is an ideal of definition of $A$ if the $q$-adic and $m_A$-adic topologies of $A$ coincide.