true of the $R$-submodule $E_{\partial}(R_f \cdot m) \subset M_f$, where here we are regarding $M_f$ as a ${\mathcal{D}}$-module in the obvious way (and replacing $R$ with $R_f$ in our definition of the $E_{\partial}$ construction). Therefore, for some $p \geq 1$, $E_{\partial}(R_f \cdot m) = R_f \cdot m + R_f \cdot \partial(m) + \cdots + R_f \cdot \partial^{p-1}(m)$, and consequently $\partial^p(m)$ can be written $\rho_0 m + \rho_1 \partial(m) + \cdots + \rho_{p-1} \partial^{p-1}(m)$ for some $\rho_0, \ldots, \rho_{p-1} \in R_f$. Clearing denominators (and multiplying by a further power of $f$ if necessary), we see that there exists $s \geq 0$ such that $f^s \partial^p(m) = r_0 m + r_1 \partial(m) + \cdots r_{p-1} \partial^{p-1}(m)$ for some $r_0, \ldots, r_{p-1} \in R$. Write $N$ for the $R$-submodule $\sum_{i=0}^{p-1} R \cdot \partial^i(m)$ of $M$. Then the fact that $f^s \partial^p(m) \in N$ implies that $f^s \partial(N) \subset N$, from which it follows at once that $E_{f^s \partial}(N) \subset N$. By definition, $N$ is a finitely generated $R$-module, so $E_{f^s \partial}(N)$ and its $R$-submodule $E_{f^s \partial}(m)$ are finitely generated $R$-modules, completing the proof.

Lemma \[reglink\] is useful because its hypothesis is satisfied for *every* holonomic ${\mathcal{D}}$-module.

[@example Prop. 1]\[fgloc\] Let $M$ be a 