Let $\log$ be the D865: Standard natural real logarithm function.
Let $x_1, \ldots, x_N \in (0, \infty)$ each be a D5407: Positive real number.

Then \begin{equation} \log(x_1 x_2 \cdots x_N) = \log(x_1) + \log(x_2) + \cdots + \log(x_N) \end{equation}