let x0, x1 be Real; :: thesis: ( x0 > 0 & x1 > 0 implies (log (number_e,x0)) - (log (number_e,x1)) = log (number_e,(x0 / x1)) )
assume A1: ( x0 > 0 & x1 > 0 ) ; :: thesis: (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; :: thesis: verum