Theorem 5.16.1448A7E9240D09

Proof. On $X\times X$, with projections $p_1,p_2$, consider $\Phi=\varphi\circ p_1+\psi\circ p_2$. The external-product identity in the proved restriction and product theorem gives \[\mathcal I(\Phi)=p_1^*\mathcal I(\varphi)\,p_2^*\mathcal I(\psi).\] Restrict to the diagonal $\iota:X\to X\times X$. The restriction part of that theorem gives $\mathcal I(\iota^*\Phi)\subseteq\mathcal I(\Phi)|_X^{\mathrm{im}}$. Here $\iota^*\Phi=\varphi+\psi$, and the image ideal on the right is $\mathcal I(\varphi)\mathcal I(\psi)$. This proves the inclusion stalkwise and hence as sheaves. The earlier theorem includes the weighted extension proof needed for the restriction step.