theorem Th3: :: DIFF_4:3

for x being Real st x > 0 holds
log (number_e,x) = ln . x