Weak partial derivatives of a compactly supported map extend by zero to all of $\mathbb{C}$

Let $E$ be a finite-dimensional real normed space, let $U\subseteq\mathbb{C}$ be open, and let $1\le p\le\infty$. Let $\xi:\mathbb{C}\to E$ be continuous with compact support $K=\operatorname{tsupport}\xi\subseteq U$, and suppose $\xi$ has weak partial derivatives $\xi_s,\xi_t$ on $U$ with $\xi_s,\xi_t\in L^p(U)$. Then:

1. the maps $\mathbf 1_K\xi_s$ and $\mathbf 1_K\xi_t$ (equal to $\xi_s$, $\xi_t$ on $K$ and to $0$ elsewhere) are weak partial derivatives of $\xi$ on all of $\mathbb{C}$;
2. $\xi_s=\mathbf 1_K\xi_s$ and $\xi_t=\mathbf 1_K\xi_t$ almost everywhere on $U$; equivalently, $\xi_s$ and $\xi_t$ vanish almost everywhere on $U\setminus K$.

This lets a compactly supported $W^{1,p}$ map on an open set be treated as a $W^{1,p}$ map on the whole plane.

Formalization Note Weak partial derivatives are HasWeakPartialsOn, tested against real $C^\infty$ functions with compact support in the given open set; $\partial_s$ is the derivative in direction $1$ and $\partial_t$ in direction $i$. $p$ is an ENNReal; $L^p(U)$ membership is MemLp for Lebesgue measure restricted to $U$. The support $K$ is the closed support tsupport ξ, and $\mathbf 1_K f$ is (tsupport ξ).indicator f.