Considering $f:X\to \mathbb{C}$, $g:X\to \mathbb{C}$ and $f\oplus g:(x,y)\mapsto f(x)+g(y)$. The Sebastiani-Thom isomorphism is an isomorphism $\Phi_{f\oplus g}(M\boxtimes N) = \Phi_{f}(M) \otimes \Phi_{g}(N)$ compatible with monodromies.

The original theorem was for constant coefficient $M = \mathbb{C}_X$, $N = \mathbb{C}_Y$. David Massey gave a proof for general constructible coefficients. Is there an algebraic proof for D-modules?

All proofs use topological arguments that don't seem to translate. In his article "On microlocal b-funtions" Saito mentions a result to be published but I couldn't find it.