[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!$.
[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]
[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]
