let x0, x1 be Real; :: thesis: ( x0 > 0 & x1 > 0 implies (ln . x0) - (ln . x1) = ln . (x0 / x1) )
assume A1: ( x0 > 0 & x1 > 0 ) ; :: thesis: (ln . x0) - (ln . x1) = ln . (x0 / x1)
A2: log (number_e,(x0 / x1)) = ln . (x0 / x1)

proof

x0 / x1 in right_open_halfline 0

proof

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

end;

hence log (number_e,(x0 / x1)) = ln . (x0 / x1) by TAYLOR_1:def 2; :: thesis: verum

end;

(ln . x0) - (ln . x1) = (log (number_e,x0)) - (ln . x1) by A1, Th3
.= (log (number_e,x0)) - (log (number_e,x1)) by A1, Th3
.= log (number_e,(x0 / x1)) by A1, Th1 ;
hence (ln . x0) - (ln . x1) = ln . (x0 / x1) by A2; :: thesis: verum