[proofplan]
We represent each operator by a symbol of the corresponding order, up to a smoothing remainder. The pseudodifferential composition theorem then produces a composed symbol of order $m+m'$ whose quantisation agrees with the principal composition modulo a smoothing operator. Since smoothing operators are absorbed into every pseudodifferential order, all remainder terms lie in $\Psi^{m+m'}(U)$. Specialising to $m=m'=0$ gives closure of $\Psi^0(U)$ under composition, while associativity is inherited from composition of linear operators.
[/proofplan]
[step:Represent the two operators by properly supported symbols modulo smoothing remainders]
Let $C_c^\infty(U)$ denote the space of smooth compactly supported complex-valued functions on $U$, and let $C^\infty(U)$ denote the space of smooth complex-valued functions on $U$. Let
\begin{align*}
A: C_c^\infty(U) \to C^\infty(U)
\end{align*}
be an operator in $\Psi^m(U)$, and let
\begin{align*}
B: C_c^\infty(U) \to C^\infty(U)
\end{align*}
be an operator in $\Psi^{m'}(U)$. For $r \in \mathbb{R}$, the notation $S^r(U \times \mathbb{R}^n)$ denotes the order-$r$ Hörmander symbol class on $U \times \mathbb{R}^n$. By the definition of $\Psi^r(U)$ in the properly supported local calculus, we may choose properly supported quantised representatives and properly supported smoothing remainders. Thus there exist symbols
\begin{align*}
a: U \times \mathbb{R}^n \to \mathbb{C}
\end{align*}
with $a \in S^m(U \times \mathbb{R}^n)$ and
\begin{align*}
b: U \times \mathbb{R}^n \to \mathbb{C}
\end{align*}
with $b \in S^{m'}(U \times \mathbb{R}^n)$, together with properly supported smoothing operators
\begin{align*}
R_A: C_c^\infty(U) \to C^\infty(U), \qquad R_B: C_c^\infty(U) \to C^\infty(U),
\end{align*}
such 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 the chosen properly supported local quantisations of the symbols $a$ and $b$, and
\begin{align*}
A = \operatorname{Op}(a) + R_A
\end{align*}
and
\begin{align*}
B = \operatorname{Op}(b) + R_B.
\end{align*}
These equalities are equalities of continuous linear maps from $C_c^\infty(U)$ to $C^\infty(U)$.
Because $A$ and $B$ are properly supported, the composition $A \circ B$ is well-defined on $C_c^\infty(U)$ and is again properly supported. Indeed, proper support means that the projections of the support of each Schwartz kernel to either factor of $U \times U$ are proper maps, and the corresponding properness condition is preserved under kernel composition.
[/step]
[step:Apply the symbolic composition theorem to the properly supported principal parts]
The operators $\operatorname{Op}(a)$ and $\operatorname{Op}(b)$ are properly supported by construction, and their symbols satisfy $a \in S^m(U \times \mathbb{R}^n)$ and $b \in S^{m'}(U \times \mathbb{R}^n)$. Therefore the symbolic composition theorem for properly supported pseudodifferential operators applies and gives a symbol
\begin{align*}
c: U \times \mathbb{R}^n \to \mathbb{C}
\end{align*}
with
\begin{align*}
c \in S^{m+m'}(U \times \mathbb{R}^n)
\end{align*}
such that
\begin{align*}
\operatorname{Op}(a) \circ \operatorname{Op}(b) - \operatorname{Op}(c)
\end{align*}
is a properly supported smoothing operator. Denote this properly supported smoothing operator by
\begin{align*}
R_0: C_c^\infty(U) \to C^\infty(U).
\end{align*}
Thus
\begin{align*}
\operatorname{Op}(a) \circ \operatorname{Op}(b) = \operatorname{Op}(c) + R_0.
\end{align*}
[/step]
[step:Absorb every smoothing remainder into order $m+m'$]
Using the decompositions of $A$ and $B$, expand the composition as
\begin{align*}
A \circ B = \bigl(\operatorname{Op}(a) + R_A\bigr) \circ \bigl(\operatorname{Op}(b) + R_B\bigr).
\end{align*}
By bilinearity of operator composition, this gives
\begin{align*}
A \circ B = \operatorname{Op}(a) \circ \operatorname{Op}(b) + \operatorname{Op}(a) \circ R_B + R_A \circ \operatorname{Op}(b) + R_A \circ R_B.
\end{align*}
Substituting the symbolic composition formula from the previous step,
\begin{align*}
A \circ B = \operatorname{Op}(c) + R_0 + \operatorname{Op}(a) \circ R_B + R_A \circ \operatorname{Op}(b) + R_A \circ R_B.
\end{align*}
Each of $R_0$, $\operatorname{Op}(a) \circ R_B$, $R_A \circ \operatorname{Op}(b)$, and $R_A \circ R_B$ is smoothing: $R_0$ is smoothing by construction, while $\operatorname{Op}(a)$, $\operatorname{Op}(b)$, $R_A$, and $R_B$ are properly supported, so the two-sided ideal property of properly supported smoothing operators applies to the remaining three compositions. Moreover, smoothing operators belong to every pseudodifferential order. Hence their sum is an element of $\Psi^{m+m'}(U)$.
Since $c \in S^{m+m'}(U \times \mathbb{R}^n)$, the operator $\operatorname{Op}(c)$ belongs to $\Psi^{m+m'}(U)$. Therefore
\begin{align*}
A \circ B \in \Psi^{m+m'}(U).
\end{align*}
[guided]
We now check carefully why the smoothing errors do not affect the final order. From the first step, the two operators have the form
\begin{align*}
A = \operatorname{Op}(a) + R_A
\end{align*}
and
\begin{align*}
B = \operatorname{Op}(b) + R_B,
\end{align*}
where $a \in S^m(U \times \mathbb{R}^n)$, $b \in S^{m'}(U \times \mathbb{R}^n)$, and $R_A,R_B$ are smoothing operators.
Expanding the product is legitimate because composition of linear operators is bilinear wherever the compositions are defined, and the chosen representatives $\operatorname{Op}(a)$, $\operatorname{Op}(b)$, $R_A$, and $R_B$ are all properly supported. Proper support guarantees that these compositions are defined on $C_c^\infty(U)$. Thus
\begin{align*}
A \circ B = \operatorname{Op}(a) \circ \operatorname{Op}(b) + \operatorname{Op}(a) \circ R_B + R_A \circ \operatorname{Op}(b) + R_A \circ R_B.
\end{align*}
The only term that contributes a genuine symbol of finite order is the first one. The pseudodifferential composition theorem says that, for properly supported quantisations of symbols $a \in S^m(U \times \mathbb{R}^n)$ and $b \in S^{m'}(U \times \mathbb{R}^n)$, there is a symbol
\begin{align*}
c: U \times \mathbb{R}^n \to \mathbb{C}
\end{align*}
with
\begin{align*}
c \in S^{m+m'}(U \times \mathbb{R}^n)
\end{align*}
such that
\begin{align*}
\operatorname{Op}(a) \circ \operatorname{Op}(b) = \operatorname{Op}(c) + R_0,
\end{align*}
where $R_0$ is properly supported and smoothing. This is exactly where the filtration order is added: the order $m$ of $a$ and the order $m'$ of $b$ combine to give the order $m+m'$ of $c$.
Substituting this identity into the expansion gives
\begin{align*}
A \circ B = \operatorname{Op}(c) + R_0 + \operatorname{Op}(a) \circ R_B + R_A \circ \operatorname{Op}(b) + R_A \circ R_B.
\end{align*}
Now we use the ideal property of smoothing operators. The representatives $\operatorname{Op}(a)$ and $\operatorname{Op}(b)$ are properly supported, and the remainders $R_A$ and $R_B$ were chosen properly supported. Since smoothing operators have smooth Schwartz kernels, composing a properly supported smoothing operator on either side with a properly supported pseudodifferential operator again gives a smoothing operator. Therefore the three terms
\begin{align*}
\operatorname{Op}(a) \circ R_B, \qquad R_A \circ \operatorname{Op}(b), \qquad R_A \circ R_B
\end{align*}
are properly supported smoothing operators, and $R_0$ is already properly supported and smoothing by construction.
Finally, smoothing operators are of order $-\infty$, meaning that they lie in $\Psi^r(U)$ for every $r \in \mathbb{R}$. In particular, all smoothing terms above lie in $\Psi^{m+m'}(U)$. Since $c \in S^{m+m'}(U \times \mathbb{R}^n)$, its quantisation $\operatorname{Op}(c)$ belongs to $\Psi^{m+m'}(U)$. Adding an operator in $\Psi^{m+m'}(U)$ to smoothing operators still gives an operator in $\Psi^{m+m'}(U)$. Hence
\begin{align*}
A \circ B \in \Psi^{m+m'}(U).
\end{align*}
[/guided]
[/step]
[step:Specialize to order zero to obtain the algebra property]
Set $m=0$ and $m'=0$. The inclusion already proved gives
\begin{align*}
\Psi^0(U) \circ \Psi^0(U) \subset \Psi^0(U).
\end{align*}
Thus $\Psi^0(U)$ is closed under composition. The operation is associative because composition of linear operators is associative on its common domain. Therefore $\Psi^0(U)$ is an algebra under composition. This proves both the filtered inclusion and the stated algebra property.
[/step]
