let a, b, c be Real; :: thesis: ( c > 1 & c to_power a = c to_power b implies a = b )
assume that
A1: c > 1 and
A2: c to_power a = c to_power b ; :: thesis: a = b
assume a <> b ; :: thesis: contradiction
then ( a < b or a > b ) by XXREAL_0:1;
hence contradiction by A1, A2, POWER:39; :: thesis: verum