let x, y be Real; :: thesis: ( 0 < x & 0 < y implies ln . (x * y) = (ln . x) + (ln . y) )
assume A1: ( 0 < x & 0 < y ) ; :: thesis: ln . (x * y) = (ln . x) + (ln . y)
then A2: ( x in right_open_halfline 0 & y in right_open_halfline 0 ) by XXREAL_1:235;
a2: x * y in right_open_halfline 0 by XXREAL_1:235, A1;
A3: number_e > 1 by XXREAL_0:2, TAYLOR_1:11;
ln . (x * y) = log (number_e,(x * y)) by a2, TAYLOR_1:def 2, TAYLOR_1:def 3
.= (log (number_e,x)) + (log (number_e,y)) by POWER:53, A1, A3
.= (log (number_e,x)) + ((log_ number_e) . y) by TAYLOR_1:def 2, A2
.= (ln . x) + (ln . y) by TAYLOR_1:def 3, TAYLOR_1:def 2, A2 ;
hence ln . (x * y) = (ln . x) + (ln . y) ; :: thesis: verum