Let $f : \mathbb{R} \to \mathbb{R}$ be a D4364: Real function such that

(i)	\begin{equation} \forall \, x \in \mathbb{R} : f(x) = x^2 \end{equation}

Let $L : \mathbb{R} \to \mathbb{R}$ be a D4364: Real function such that

(i)	$x_0 \in \mathbb{R}$ is a D993: Real number
(ii)	\begin{equation} \forall \, x \in \mathbb{R} : L(x) = 2 x_0 x \end{equation}

Then $L$ is a D5681: Real function derivative for $f$ at $x_0$.