If $E_i$ is a $\mathbb R$-Banach space and $\Omega_1\subseteq E_1$, then $f:\Omega_1\to E_2$ is called $C^1$-differentiable at $x_1\in\Omega_1$ if $$\left.f\right|_{O_1\:\cap\:\Omega_1}=\left.\tilde f\right|_{O_1\:\cap\:\Omega_1}$$ for some $\tilde f\in C^1(O_1,E_2)$ for some $E_1$-open neighborhood $O_1$ of $x_1$.
Is $${\rm D}f(x_1):={\rm D}\tilde f(x_1)\tag1$$ well-defined, i.e. independent of the choice of $\tilde f$?
I would say, it obviously should be, but the discussion below this question raised some doubts.
Maybe I'm missing subtlety but if $\hat O_1$ and $\hat f$ are other choices for $O_1$ and $\tilde f$, then there is a $\varepsilon>0$ such that the $E_1$-open ball around $x$ with radius $\varepsilon$ is contained in $O_1\cap\hat O_1$ and it should clearly hold \begin{equation}\begin{split}&\left\|\left({\rm D}\tilde f(x_1)-{\rm D}\hat f(x_1)\right)h_1\right\|_{E_2}\\&=\left\|\frac{\hat f(x_1+h_1)-\hat f(x_1)-{\rm D}\hat f(x_1)h_1}{\left\|h_1\right\|_{E_1}}-\frac{\tilde f(x_1+h_1)-\tilde f(x_1)-{\rm D}\tilde f(x_1)h_1}{\left\|h_1\right\|_{E_1}}\right\|_{E_2}\left\|h_1\right\|_{E_1}\end{split}\end{equation} for all $h_1\in E_1\setminus\{0\}$ with $\left\|h\right\|_{E_1}<\varepsilon$, which tends to $0$ as $h\to0$. So, it should hold $${\rm D}\tilde f(x_1)={\rm D}\hat f(x_1)\tag2.$$ What am I missing?
Consider $f\colon\mathbb{R}\times\{0\}\rightarrow\mathbb{R}^2,\,(x,0)\mapsto(x,0)$. Consider $\operatorname{id}\colon\mathbb{R}^2\rightarrow\mathbb{R}^2$ and $\pi\colon\mathbb{R}^2\rightarrow\mathbb{R}^2,\,(x,y)\mapsto(x,0)$. Both of these are differentiable (smooth even) functions and clearly $\operatorname{id}\vert_{\mathbb{R}\times\{0\}}=f=\pi\vert_{\mathbb{R}\times\{0\}}$. However, $D\operatorname{id}(x)=\operatorname{id}\neq\pi=D\pi(x)$ for any $x\in\mathbb{R}^2$.