holonomic ${\mathcal{D}}$-module. There exists a nonzero $f \in R$ such that $M_f$ is a finitely generated $R_f$-module.

We first consider two special cases. If $M$ is $R$-torsionfree, this is [@bjork Lemma 3.3.19]. If $M$ is simple as a ${\mathcal{D}}$-module and is not $R$-torsionfree, there exist nonzero $f \in R$ and $m \in M$ such that $fm = 0$. By the simplicity of $M$, $M = {\mathcal{D}}\cdot m$, from which it follows that $M_f$ is zero and *a fortiori* finitely generated. To prove the proposition for all holonomic ${\mathcal{D}}$-modules $M$, we use the fact that any such $M$ is of finite length as a ${\mathcal{D}}$-module. If $$0 \rightarrow M' \rightarrow M \rightarrow M'' \rightarrow 0$$ is a short exact sequence of ${\mathcal{D}}$-modules and there exist nonzero $g,h \in R$ such that $M'_f$ (resp. $M''_g$) is a finitely generated $R_f$- (resp. $R_g$-) module, then $M_{fg}$ is a finitely generated $R_{fg}$-module. Therefore induction on length, which reduces us to the case of a simple ${\mathcal{D}}$-module and hence to the previous two special cases, completes the proof.

Recall from section \[prelim\] that $f \in R$ is said to be *$x_n$-regular* if $f(0,0,\ldots, 0, x_n) \neq 0$, in which case $f$ can be written as 