let a, b, c, x be Real; :: thesis: for n being Element of NAT st a <> 0 & b / a < 0 & c / a > 0 & ex m being Element of NAT st
( n = 2 * m & m >= 1 ) & delta a,b,c >= 0 & Polynom a,b,c,(x |^ n) = 0 & not x = n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a)) & not x = - (n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a))) & not x = n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a)) holds
x = - (n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a)))
let n be Element of NAT ; :: thesis: ( a <> 0 & b / a < 0 & c / a > 0 & ex m being Element of NAT st
( n = 2 * m & m >= 1 ) & delta a,b,c >= 0 & Polynom a,b,c,(x |^ n) = 0 & not x = n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a)) & not x = - (n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a))) & not x = n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a)) implies x = - (n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a))) )
assume A1: ( a <> 0 & b / a < 0 & c / a > 0 & ex m being Element of NAT st
( n = 2 * m & m >= 1 ) & delta a,b,c >= 0 & Polynom a,b,c,(x |^ n) = 0 ) ; :: thesis: ( x = n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a))) )
A2: ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) > 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) > 0 ) by A1, Th1;

now

per cases ( x |^ n = ((- b) + (sqrt (delta a,b,c))) / (2 * a) or x |^ n = ((- b) - (sqrt (delta a,b,c))) / (2 * a) ) by A1, POLYEQ_1:5;

suppose x |^ n = ((- b) + (sqrt (delta a,b,c))) / (2 * a) ; :: thesis: ( x = n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a))) )

hence ( x = n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a))) ) by A1, A2, Th4; :: thesis: verum

end;

suppose x |^ n = ((- b) - (sqrt (delta a,b,c))) / (2 * a) ; :: thesis: ( x = n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a))) )

hence ( x = n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a))) ) by A1, A2, Th4; :: thesis: verum

end;

end;

end;

hence ( x = n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta a,b,c))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta a,b,c))) / (2 * a))) ) ; :: thesis: verum