theorem :: NUMBER13:47

for n, x, y, z being positive Nat holds
( (n |^ x) + (n |^ y) = n |^ z iff ( n = 2 & y = x & z = x + 1 ) )