[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*}[/step]

[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: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]