I came across the following theorem in Foundations of mechanics by Ralph Abraham
Let $M$ be a smooth manifold. Suppose for each open $U\subset M $, we have maps $E_U: C^\infty(U) \to C^\infty(U)$ and $F_U:\mathfrak{X}(U) \to \mathfrak{X}(U)$, which are $\mathbb{R}$-linear tensor derivations and natural with respect to restrictions, i.e.
1) $E_U (f\otimes g) = (E_U f)\otimes g + f\otimes (E_U g)$
2) $E_U(f |_U) = (E_M f)|_U $
3) $F_U(f\otimes X) = (E_U f)\otimes X + f\otimes (F_U X) $
4) $F_U(X_U) = (F_M X)|_U $
Then there exists a unique differential operator $D$ on the whole tensor algebra $\mathcal{T}(M)$ that coincides with $E_U$ on $C^\infty(U)$ and with $F_U$ on $\mathfrak{X}(U)$.
So the proof of uniqueness is quite clear for me, but I'm struggling a bit with the existence part.
Note that any differential operator $D$ on $\mathcal{T}(M)$ is defined to be local with respect to restrictions, i.e. for opens sets $U\subset V\subset M$ and $t\in \mathcal{T}^r_s(V)$ one has $(Dt)_U = D(t_U) \in \mathcal{T}^r_s(U)$.
In the proof of uniqueness one can make use of this and restrict oneself to coordinate charts. So let $U$ be a chart neighborhood and $t\in \mathcal{T}^r_s(U)$ such that $t=t^{i_1\cdots i_r}_{j_1\cdots j_s} \frac{\partial}{\partial x^i_1} \otimes \cdots \otimes \text{d}x^{j_s}$. Using the fact that $D$ is a tensor derivation, one obtains the local expression
$$Dt=E_U(t^{i_1\cdots i_r}_{j_1\cdots j_s})\frac{\partial}{\partial x^i_1} \otimes \cdots \otimes \text{d}x^{j_s} + t^{i_1\cdots i_r}_{j_1\cdots j_s} F_U \left(\frac{\partial}{\partial x^i_1}\right) \otimes \cdots \otimes \text{d}x^{j_s} + \cdots + t^{i_1\cdots i_r}_{j_1\cdots j_s}\frac{\partial}{\partial x^i_1} \otimes \cdots \otimes D(\text{d}x^{j_s}) $$
where $D(\text{d}x^j)$ is uniquely determined through another definining property of $D$, namely that $D\delta=0$, where $\delta$ is Kronecker's delta.
For existence, the first step is to define $D$ acting on any tensor field by the above local expression. And here is where I'm having problems to explicitly show that such a $D$ is natural with respect to restrictions. I thought about that one could just make a simple pointwise argument. This would imply though, that if we define any object by their local chart expressions, that as long as they agree on overlaps, they define a global object which is natural with respect to restrictions. However, I'm not sure if this implication is correct and if I make it too easy for me.
So at the moment, my guess is that I'm missing something and one actually has to use $2)$ and $4)$ explicitly.
Any help is appreciated.
Showing that $D$ is natural with respect to restrictions is essentially by definitions. $D$ is locally on coordinate patches so that it already respects overlapping charts. The fact that defining objects by local chart expressions which agree on overlaps yields well defined global objects is a result of the fact that the sections of a tensor bundle $\mathcal{T}^r_s$ form a sheaf, in particular they satisfy the following:
We denote the sections of $\mathcal{T}^r_s$ on an open set $U\subset M$ by $\mathcal{E}(U)$. Given an open cover of $M$, $\{U_{\alpha}\}_{\alpha\in A}$, and a collection of sections $\sigma_{\alpha}\in \mathcal{E}(U_{\alpha})$ for each $\alpha\in A$ such that for $\beta,\gamma\in A$ we have $\sigma_{\beta}\vert_{U_{\beta}\cap U_{\gamma}}=\sigma_{\gamma}\vert_{U_\beta\cap U_\gamma}$ there exists $\sigma\in\mathcal{E}(M)$ such that $\sigma\vert_{U\alpha}=\sigma_{\alpha}$. In plain english, this means that if I specify the data of sections of $\mathcal{T}^r_s$ on an open cover of $M$, e.g. coordinate neighborhoods of $M$, which agree on overlaps, these glue together into a global section which restricts to the starting data.