theorem :: DIFF_4:2

for x0, x1 being Real st x0 > 0 & x1 > 0 holds
(log (number_e,x0)) + (log (number_e,x1)) = log (number_e,(x0 * x1))