let a, b be positive Real; :: thesis: ( a <> b implies ex n, m being Real st
( a = (a / b) to_power n & b = (a / b) to_power m ) )
assume A1: a <> b ; :: thesis: ex n, m being Real st
( a = (a / b) to_power n & b = (a / b) to_power m )
reconsider x = a / b as positive Real ;
x <> 1 by A1, XCMPLX_1:58;
then ( x to_power (log (x,a)) = a & x to_power (log (x,b)) = b ) by POWER:def 3;
hence ex n, m being Real st
( a = (a / b) to_power n & b = (a / b) to_power m ) ; :: thesis: verum