I am reading Francois Treves' Introduction to pseudodifferential and Fourier integral operators, vol. I.
Let $\Omega \subseteq \mathbb{R}^n$ be open. On page 11, Treves defines what it means for a continuous linear map $K : C_c^\infty(\Omega) \to \mathcal{D}'(\Omega)$ to be regularizing. $K$ is called regularizing if and only if $K$ extends to a continuous linear map $\mathcal{E}'(\Omega) \to C^\infty(\Omega)$.
Then Treves states the following proposition.
If $K : C^\infty_c(\Omega) \to \mathcal{D}'(\Omega)$ is regularizing, then the associated Schwartz kernel $k \in \mathcal{D}'(\Omega \times \Omega)$ is in $C^\infty(\Omega \times \Omega)$.
I am trying to prove this, and here's what I have so far. It is enough to show that $k$ is $C^\infty(\Omega \times \Omega)$ on tensor products since they are dense in $\mathcal{D}(\Omega \times \Omega)$. So let $\varphi, \psi \in C_c^\infty(\Omega)$. Use the statement of the Schwartz Kernel Theorem, and the fact that $K\psi \in C^\infty (\Omega)$ (since $\psi \in \mathcal{E}'(\Omega))$, to get
$$\langle k, \varphi \otimes \psi \rangle = \langle K\psi , \varphi \rangle = \int_\Omega (K\psi)(x)\varphi(x)dx.$$
But what I really want is some smooth function $k(x,y)$ of two variables, integrated against $\varphi \otimes \psi$. That is, what I want is
$$\langle k, \varphi \otimes \psi \rangle = \int_\Omega \int_\Omega k(x,y)(\varphi \otimes \psi)(x,y)dxdy$$.
Unfortunately, I am stuck and can't move further with the calculation. Hints or solutions are greatly appreciated!
This result can be found in the Hormander's book, The Analysis of Linear Partial Differential Operators I. More precisely, Theorem 5.2.6., page 132.