ThmDex – An index of mathematical definitions, results, and conjectures.
P3580
If $f = a \exp$, then from the results
(i) R5254: Slope function for standard natural real exponential function
(ii) R4285: Standard natural real exponential function maps zero to one

we know that conditions (1) and (2) hold.

Conversely, assume that the conditions (1) and (2) hold. Using the results
(i) R5255: Slope function for pointwise product of two differentiable real functions
(ii) R5256: Slope function for composition of two differentiable real functions

and the assumption $f' = f$, we have \begin{equation} \frac{d}{d x} f(x) \exp(- x) = f'(x) \exp(- x) - f(x) \exp(- x) = f'(x) \exp(- x) - f'(x) \exp(- x) = 0 \end{equation} for every $x \in \mathbb{R}$. That is, the function \begin{equation} x \mapsto f(x) \exp(- x) = \frac{f(x)}{\exp(x)} \end{equation} is constant everywhere on $\mathbb{R}$. Since $f(0) = a$, then $f(0) \exp(-0) = a \exp(0) = a$. That is, $f(x) \exp(-x) = a$ and equivalently $f(x) = a \exp(x)$ for every $x \in \mathbb{R}$. $\square$