[proofplan] The proof extracts the first two homogeneous levels from the left-quantized symbolic composition expansion stated in the theorem hypothesis. That expansion says that truncating the sum of composition terms before total multi-index order $N$ leaves an error in $S^{m+m'-N}_{1,0}$. Taking $N=1$ gives the principal product $ab$, while taking $N=2$ retains exactly the zero-order term and the first-order multi-index terms. Symbol estimates show that the remaining terms have order at most $m+m'-2$, which is precisely the asserted quotient statement. [/proofplan]

[step:Apply the left-quantized symbolic composition expansion]By the left-quantized symbolic composition expansion assumed in the theorem statement, the localized or properly supported hypotheses ensure that the composition symbol $c$ admits the following asymptotic expansion in the symbol scale on $V \times \mathbb{R}^n$: for every integer $N \geq 1$, \begin{align*} c - \sum_{|\alpha|<N}\frac{1}{\alpha!}\partial_\xi^\alpha a\,D_x^\alpha b \in S^{m+m'-N}_{1,0}(V \times \mathbb{R}^n). \end{align*} Here $|\alpha| := \alpha_1+\cdots+\alpha_n$ and $\alpha! := \alpha_1!\cdots \alpha_n!$.[/step]

[guided]The composition formula is the only pseudodifferential input. Because the quantization is left quantization and the differential convention is that $D_{x_j}$ denotes $-i\partial_{x_j}$, the expansion is exactly the one assumed in the theorem statement. The localization assumption $V \Subset U$, or alternatively proper support of the representatives, is what makes the composition symbol well-defined on the patch without uncontrolled support terms. The precise meaning of the asymptotic symbol expansion is that truncating before total multi-index order $N$ leaves an error of order $m+m'-N$: \begin{align*} c - \sum_{|\alpha|<N}\frac{1}{\alpha!}\partial_\xi^\alpha a\,D_x^\alpha b \in S^{m+m'-N}_{1,0}(V \times \mathbb{R}^n). \end{align*} This is the mechanism that separates the principal term, the first correction, and the lower-order remainder.[/guided]

[step:Extract the zero multi-index term to identify the principal symbol] Take $N=1$ in the expansion. The only multi-index satisfying $|\alpha|<1$ is $\alpha=0$, and for this multi-index one has $\alpha!=1$, $\partial_\xi^\alpha a=a$, and $D_x^\alpha b=b$. Hence \begin{align*} c - ab \in S^{m+m'-1}_{1,0}(V \times \mathbb{R}^n). \end{align*} Since $ab \in S^{m+m'}_{1,0}(V \times \mathbb{R}^n)$ by the standard product estimate for $(1,0)$-symbols, the class of $c$ modulo $S^{m+m'-1}_{1,0}(V \times \mathbb{R}^n)$ is represented by $ab$. [/step]

[step:Retain the first-order multi-index terms] Take $N=2$ in the expansion. The multi-indices satisfying $|\alpha|<2$ are $\alpha=0$ and the standard basis multi-indices $e_1,\dots,e_n$, where $e_j$ has $1$ in the $j$th component and $0$ elsewhere. For $\alpha=e_j$, one has $\alpha!=1$, $\partial_\xi^\alpha a=\partial_{\xi_j}a$, and $D_x^\alpha b=D_{x_j}b$. Therefore \begin{align*} c - ab - \sum_{j=1}^n \partial_{\xi_j}a\,D_{x_j}b \in S^{m+m'-2}_{1,0}(V \times \mathbb{R}^n). \end{align*} Equivalently, modulo $S^{m+m'-2}_{1,0}(V \times \mathbb{R}^n)$, \begin{align*} c(x,\xi) \equiv a(x,\xi)b(x,\xi)+\sum_{j=1}^n \partial_{\xi_j}a(x,\xi)D_{x_j}b(x,\xi). \end{align*} [/step]

[step:Check that the displayed terms have the asserted symbolic orders] For each $j \in \{1,\dots,n\}$, the symbol estimate for $\partial_{\xi_j}a$ gives \begin{align*} \partial_{\xi_j}a \in S^{m-1}_{1,0}(V \times \mathbb{R}^n). \end{align*} Since $x$-derivatives do not lower order in the $S^m_{1,0}$ scale, \begin{align*} D_{x_j}b \in S^{m'}_{1,0}(V \times \mathbb{R}^n). \end{align*} The product estimate for symbols then gives \begin{align*} \partial_{\xi_j}a\,D_{x_j}b \in S^{m+m'-1}_{1,0}(V \times \mathbb{R}^n). \end{align*} Thus the correction term has order $m+m'-1$, and the symbolic expansion with $N=2$ places all omitted terms in $S^{m+m'-2}_{1,0}(V \times \mathbb{R}^n)$. This proves both the principal symbol assertion and the stated first correction formula. [/step]