theorem Lm6: :: ASYMPT_2:10

ex g being PartFunc of REAL,REAL st
( dom g = right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds
g . x = log (2,x) ) & g is_differentiable_on right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds
( g is_differentiable_in x & diff (g,x) = (log (2,number_e)) / x & 0 < diff (g,x) ) ) )