theorem Th48: :: NUMBER13:48
for a, b, c being Real st c > 1 & c to_power a = c to_power b holds
a = b