Let $\log : (0, \infty) \to \mathbb{R}$ be the D865: Standard natural real logarithm function.
Let $L : \mathbb{R} \to \mathbb{R}$ be a D4364: Real function such that

(i)	$x_0 \in (0, \infty)$ is a D5407: Positive real number
(ii)	\begin{equation} \forall \, x \in \mathbb{R} : L(x) = \frac{1}{x_0} x \end{equation}

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