let k, m, n be Nat; :: thesis: ( k > 1 & k |^ n = k |^ m implies n = m )
assume that
A1: k > 1 and
A2: k |^ n = k |^ m ; :: thesis: n = m

now :: thesis: n = m

per cases ( n = m or n <> m ) ;

suppose n = m ; :: thesis: n = m

hence n = m ; :: thesis: verum

end;

suppose n <> m ; :: thesis: n = m

then k to_power m <> k to_power n by A1, POWER:50;
hence n = m by A2; :: thesis: verum

end;

end;

end;

hence n = m ; :: thesis: verum