ex f being PartFunc of REAL,REAL st
( right_open_halfline number_e = dom f & ( for x being Real st x in dom f holds
f . x = x / (log (2,x)) ) & f is_differentiable_on right_open_halfline number_e & ( for x0 being Real st x0 in right_open_halfline number_e holds
0 <= diff (f,x0) ) & f is non-decreasing )