let a, x, b, y, p be Real; :: thesis:
let n be Element of NAT ; :: thesis:
assume A1: ( (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & ex m being Element of NAT st
( n = 2 * m & m >= 1 ) & p / b > 0 & p / a > 0 & a * b <> 0 ) ; :: thesis:
then consider m being Element of NAT such that
A2: ( n = 2 * m & m >= 1 ) ;
n >= 1 by A2, XREAL_1:163;
then A4: n > 0 by XXREAL_0:2;

per cases by A1, XCMPLX_1:6;

suppose A5: x = 0 ; :: thesis:

then (a * (0 to_power n)) + (b * (y |^ n)) = p by A1;
then (a * 0 ) + (b * (y |^ n)) = p by A4, POWER:def 2;
then y |^ n = p / b by A1, XCMPLX_1:90;
hence ( ( x = 0 & y = n -root (p / b) ) or ( x = 0 & y = - (n -root (p / b)) ) or ( x = n -root (p / a) & y = 0 ) or ( x = - (n -root (p / a)) & y = 0 ) ) by A1, A5, Th4; :: thesis:

end;

suppose A6: y = 0 ; :: thesis:

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

end;