Let $f : \mathbb{R} \to (0, \infty)$ be a D5614: Differentiable real function.
Let $\exp : \mathbb{R} \to (0, \infty)$ be the D1932: Standard natural real exponential function.
Let $a \in \mathbb{R}$ be a D993: Real number.
Let $\exp : \mathbb{R} \to (0, \infty)$ be the D1932: Standard natural real exponential function.
Let $a \in \mathbb{R}$ be a D993: Real number.
Then $f = a \exp$ if and only if
(1) | $\forall \, x \in \mathbb{R}: f'(x) = f(x)$ |
(2) | $f(0) = a$ |