let x0, x1 be Real; ( x0 > 0 & x1 > 0 implies (log (number_e,x0)) - (log (number_e,x1)) = log (number_e,(x0 / x1)) )
assume A1:
( x0 > 0 & x1 > 0 )
; (log (number_e,x0)) - (log (number_e,x1)) = log (number_e,(x0 / x1))
number_e > 1
by TAYLOR_1:11, XXREAL_0:2;
hence
(log (number_e,x0)) - (log (number_e,x1)) = log (number_e,(x0 / x1))
by A1, POWER:54; verum