for a, b, n being Nat st a > 0 & n > 0 holds
ex r being real number st (a |^ n) + (b |^ n) = r |^ n by Th29;