Let $U \subset \mathbb{R}^n$ be open, let $m,m' \in \mathbb{R}$, and let $a \in S^m_{1,0}(U \times \mathbb{R}^n)$ and $b \in S^{m'}_{1,0}(U \times \mathbb{R}^n)$. Let $V,W \subset U$ be open sets such that $V \Subset W \Subset U$. Choose functions $\chi,\psi \in C_c^\infty(U)$ such that $\chi = 1$ on an open neighbourhood of $\overline V$, $\operatorname{supp}\chi \subset W$, and $\psi = 1$ on an open neighbourhood of $\operatorname{supp}\chi$.

For each $\ell \in \mathbb{R}$ and each $q \in S^\ell_{1,0}(U \times \mathbb{R}^n)$, define the local left quantization $\operatorname{Op}(q): C_c^\infty(U) \to C^\infty(U)$ by the compactly supported oscillatory integral

\begin{align*} \operatorname{Op}(q)u(x) = (2\pi)^{-n}\operatorname{Os}\!\int_{\mathbb{R}^n}\int_U e^{i(x-y)\cdot \xi}q(x,\xi)u(y)\,d\mathcal{L}^n(y)\,d\mathcal{L}^n(\xi). \end{align*}

Here $\operatorname{Os}\!\int$ denotes the standard oscillatory regularization by compactly supported cutoff functions in the frequency variables. Then, after restricting output points to $V$, the localized composition $\chi\,\operatorname{Op}(a)\,\psi\,\operatorname{Op}(b)$ agrees modulo a smoothing operator $C_c^\infty(U) \to C^\infty(V)$ with a left-quantized operator $\operatorname{Op}(c)$, where $c: V \times \mathbb{R}^n \to \mathbb{C}$ belongs to $S^{m+m'}_{1,0}(V \times \mathbb{R}^n)$ and satisfies the asymptotic expansion

\begin{align*} c(x,\xi) \sim \sum_{\alpha \in \mathbb{N}_0^n}\frac{1}{\alpha!}\,\partial_\xi^\alpha a(x,\xi)\,D_x^\alpha b(x,\xi) \end{align*}

in $S^{m+m'}_{1,0}(V \times \mathbb{R}^n)$, where $D_x^\alpha = (-i)^{|\alpha|}\partial_x^\alpha$. Equivalently, for every integer $N \ge 1$,

\begin{align*} c(x,\xi)-\sum_{|\alpha|<N}\frac{1}{\alpha!}\,\partial_\xi^\alpha a(x,\xi)\,D_x^\alpha b(x,\xi) \in S^{m+m'-N}_{1,0}(V \times \mathbb{R}^n). \end{align*}

For every multi-index $\alpha \in \mathbb{N}_0^n$, the map $(x,\xi) \mapsto \alpha!^{-1}\partial_\xi^\alpha a(x,\xi)D_x^\alpha b(x,\xi)$ belongs to $S^{m+m'-|\alpha|}_{1,0}(V \times \mathbb{R}^n)$. The same formula holds after replacing $\operatorname{Op}(a)$ and $\operatorname{Op}(b)$ by properly supported operators whose kernels agree with the corresponding local left-quantized kernels near the diagonal; changing the auxiliary cutoffs or these representatives changes the localized symbol on $V$ only by a smoothing symbol in $S^{-\infty}(V \times \mathbb{R}^n)$.