theorem :: POLYEQ_4:20
for x, y, a, p, q being Real
for n being Element of NAT st a * (x |^ n) = p & x * y = q & n is odd & p * a <> 0 holds
( x = n -root (p / a) & y = q * (n -root (a / p)) )