theorem lemp: :: FIELD_16:7

for p1, p2 being Prime
for n1, n2 being Nat st ( n1 <> 0 or n2 <> 0 ) & p1 |^ n1 = p2 |^ n2 holds
( p1 = p2 & n1 = n2 )