let x, y, a, b, p be Real; :: thesis: for n being Element of NAT st (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & n is odd & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) holds
( x = n -root (p / a) & y = 0 )
let n be Element of NAT ; :: thesis: ( (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & n is odd & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) implies ( x = n -root (p / a) & y = 0 ) )
assume that
A1: (a * (x |^ n)) + (b * (y |^ n)) = p and
A2: x * y = 0 and
A3: n is odd and
A4: a * b <> 0 ; :: thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) )
consider m being Nat such that
A5: n = (2 * m) + 1 by A3, ABIAN:9;
A6: n > 0 by A5;

now :: thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) )

per cases ( x = 0 or y = 0 ) by A2;

suppose A7: x = 0 ; :: thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) )

then (a * (0 to_power n)) + (b * (y |^ n)) = p by A1;
then (a * 0) + (b * (y |^ n)) = p by A6, POWER:def 2;
then y |^ n = p / b by A4, XCMPLX_1:89;
hence ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) ) by A3, A7, POWER:4; :: thesis: verum

end;

suppose A8: y = 0 ; :: thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) )

then (a * (x |^ n)) + (b * (0 to_power n)) = p by A1;
then (a * (x |^ n)) + (b * 0) = p by A6, POWER:def 2;
then x |^ n = p / a by A4, XCMPLX_1:89;
hence ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) ) by A3, A8, POWER:4; :: thesis: verum

end;

end;

end;

hence ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) ) ; :: thesis: verum