let x0 be real number ; :: thesis: 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) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_differentiable_in x0 & f . x0 > 0 implies ( ln * f is_differentiable_in x0 & diff (ln * f),x0 = (diff f,x0) / (f . x0) ) )
assume that
A1: f is_differentiable_in x0 and
A2: f . x0 > 0 ; :: thesis: ( ln * f is_differentiable_in x0 & diff (ln * f),x0 = (diff f,x0) / (f . x0) )
A3: f . x0 in right_open_halfline 0

proof

f . x0 in { g where g is Real : 0 < g } by A2;
hence f . x0 in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum

end;

A4: ln is_differentiable_in f . x0 by A3, Th18, FDIFF_1:16;
A5: x0 is Real by XREAL_0:def 1;
hence ln * f is_differentiable_in x0 by A1, A4, FDIFF_2:13; :: thesis: diff (ln * f),x0 = (diff f,x0) / (f . x0)
thus diff (ln * f),x0 = (diff ln ,(f . x0)) * (diff f,x0) by A1, A4, A5, FDIFF_2:13
.= (1 / (f . x0)) * (diff f,x0) by A3, Th18
.= ((diff f,x0) / (f . x0)) * 1 by XCMPLX_1:76
.= (diff f,x0) / (f . x0) ; :: thesis: verum