let h, x be Real; :: thesis: ( x > 0 & x + h > 0 implies (fD (ln,h)) . x = ln . (1 + (h / x)) )
set f = ln ;
assume A1: ( x > 0 & x + h > 0 ) ; :: thesis: (fD (ln,h)) . x = ln . (1 + (h / x))
A2: x in right_open_halfline 0

proof

x in { g where g is Real : 0 < g } by A1;
hence x in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum

end;

A3: x + h in right_open_halfline 0

proof

x + h in { g where g is Real : 0 < g } by A1;
hence x + h in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum

end;

(fD (ln,h)) . x = (ln . (x + h)) - (ln . x) by A2, A3, DIFF_1:1, TAYLOR_1:18
.= ln . ((x + h) / x) by A1, Th4
.= ln . ((x / x) + (h / x))
.= ln . (1 + (h / x)) by A1, XCMPLX_1:60 ;
hence (fD (ln,h)) . x = ln . (1 + (h / x)) ; :: thesis: verum