let x be Real; :: thesis: ( x > 0 implies log (number_e,x) = ln . x )
assume A1: x > 0 ; :: thesis: log (number_e,x) = ln . x
x in right_open_halfline 0
proof
x in { g where g is Real : 0 < g } by A1;
hence x in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum
end;
hence log (number_e,x) = ln . x by TAYLOR_1:def 2; :: thesis: verum