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

now

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:57;
hence n = m by A1; :: thesis: verum

end;

end;

end;

hence n = m ; :: thesis: verum