A2: number_e <> 1 by TAYLOR_1:11;
A1: 1 in right_open_halfline 0 by XXREAL_1:235;
ln . 1 = log (number_e,1) by A1, TAYLOR_1:def 2, TAYLOR_1:def 3
.= 0 by TAYLOR_1:11, A2, POWER:51 ;
hence ln . 1 = 0 ; :: thesis: verum