hypothesis and the second is $m$, so $-m \in x_nE$. Now suppose that $m \in x_n^qE$ for some $q \geq 1$, and write $m = x_n^q \sum_{i=1}^l r_im_i$ for some $r_1, \ldots, r_l \in R$. As $m$ is an $R_{n-1}$-linear combination of elements of $M$ killed by $\partial$, we have $\partial(m) = 0$, so $\frac{1}{q!}x_n^q\partial^q m = 0$. Substituting $x_n^q \sum_{i=1}^l r_im_i$ for $m$ in the left-hand side of this equation and using the Leibniz rule, we see that the only terms which *a priori* may lack an $x_n^{q+1}$ factor are those in the sum $\sum_{i=1}^l r_{i,0}x_n^qm_i$: we obtain, for some $\mu \in E$, an expression $$0 = \frac{1}{q!}x_n^q\partial^q m = \frac{1}{q!}x_n^q\partial^q(x_n^q \sum_{i=1}^l r_im_i) = \sum_{i=1}^l r_{i,0}x_n^qm_i + x_n^{q+1}\mu,$$ so that $\sum_{i=1}^l r_{i,0}x_n^qm_i \in x_n^{q+1}E$. It follows that $m \in x_n^{q+1}E$, as $$m - \sum_{i=1}^l r_{i,0}x_n^qm_i = \sum_{i=1}^l(\sum_{s=1}^{\infty} r_{i,s}x_n^{s+q}m_i)$$ and we have an $x_n^{q+1}$ factor in every remaining term. This completes the proof.

[@kernel Thm. (iii)]\[holkernel\] Let $M$ be a holonomic ${\mathcal{D}}$-module. Then $M_*$ is a holonomic ${\mathcal{D}}_{n-1}$-module.

Consider the $R$-submodule $R \cdot M_*$ of $M$ generated by $M_*$. If $r \in R$ and $m \in M_*$, then $\partial(rm) = \partial(r)m + r\partial(m) = \partial(r)m$; since $M_*$ is already a 