Let $n\in\mathbb{N}$, let $U \subset \mathbb{R}^n$ be open, let $m,m' \in \mathbb{R}$, and let $N \in \mathbb{N}$ with $N \ge 1$. Fix the Kohn-Nirenberg quantization convention

\begin{align*} \operatorname{Op}(q)u(x)=(2\pi)^{-n}\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*}

for symbols $q:U\times\mathbb{R}^n\to\mathbb{C}$ and test functions $u\in C_c^\infty(U)$. Here an operator $T:C_c^\infty(U)\to C^\infty(U)$ is properly supported if both coordinate projections are proper on the support of its Schwartz kernel in $U\times U$, and an operator is smoothing on $U$ if its Schwartz kernel is a $C^\infty$ function on $U\times U$. For every compact set $K\subset U$ and every $r\in\mathbb{R}$, $S^r(K\times\mathbb{R}^n)$ denotes the corresponding local symbol class restricted to $K\times\mathbb{R}^n$, and

\begin{align*} S^{-\infty}(K\times\mathbb{R}^n):=\bigcap_{r\in\mathbb{R}}S^r(K\times\mathbb{R}^n). \end{align*}

Let $a:U\times\mathbb{R}^n\to\mathbb{C}$ and $b:U\times\mathbb{R}^n\to\mathbb{C}$ be Kohn-Nirenberg symbols satisfying $a\in S^m(U\times\mathbb{R}^n)$ and $b\in S^{m'}(U\times\mathbb{R}^n)$. Assume that $\operatorname{Op}(a):C_c^\infty(U)\to C^\infty(U)$ and $\operatorname{Op}(b):C_c^\infty(U)\to C^\infty(U)$ are properly supported. Let $a\# b:U\times\mathbb{R}^n\to\mathbb{C}$ be a symbol in $S^{m+m'}(U\times\mathbb{R}^n)$ such that $\operatorname{Op}(a\# b):C_c^\infty(U)\to C^\infty(U)$ is properly supported and $\operatorname{Op}(a\# b)-\operatorname{Op}(a)\operatorname{Op}(b)$ is smoothing on $U$. Then

\begin{align*} a\# b-\sum_{|\alpha|<N}\frac{i^{-|\alpha|}}{\alpha!}\,\partial_\xi^\alpha a\,\partial_x^\alpha b\in S^{m+m'-N}(U\times\mathbb{R}^n). \end{align*}