theorem :: TAYLOR_1:20

for x0 being Real
for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds
( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) )