for a, b, c, n being Nat st a > 0 & b > 0 & (a |^ n) + (b |^ n) = c |^ n holds
ex j, k, l being Nat st
( (j |^ n) + (k |^ n) = l |^ n & j,k are_coprime & j,l are_coprime & k,l are_coprime & a = (a gcd b) * j & b = (a gcd b) * k & c = (a gcd b) * l )