theorem Th30: :: PEPIN:30

for k, m, n being Nat st k > 1 & k |^ n = k |^ m holds
n = m