let h, x be Real; :: thesis: ( x > 0 & x - h > 0 implies (bD (ln,h)) . x = ln . (1 + (h / (x - h))) )
set f = ln ;
assume A1: ( x > 0 & x - h > 0 ) ; :: thesis: (bD (ln,h)) . x = ln . (1 + (h / (x - h)))
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;

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