let x0, x1 be Real; :: thesis: ( x0 > 0 & x1 > 0 implies (log (number_e,x0)) + (log (number_e,x1)) = log (number_e,(x0 * x1)) )
assume A1: ( x0 > 0 & x1 > 0 ) ; :: thesis: (log (number_e,x0)) + (log (number_e,x1)) = log (number_e,(x0 * x1))
number_e > 1 by TAYLOR_1:11, XXREAL_0:2;
hence (log (number_e,x0)) + (log (number_e,x1)) = log (number_e,(x0 * x1)) by A1, POWER:53; :: thesis: verum