let x, a, b, c be Real; :: thesis:
assume that
A1: ( a <> 0 & (((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c) > 0 ) and
A2: Polynom (a,b,c,c,b,a,x) = 0 ; :: thesis:
let y1, y2 be Real; :: thesis:
assume that
A3: y1 = ((a - b) + (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) and
A4: y2 = ((a - b) - (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) ; :: thesis:
A5: 0 = ((((x |^ 5) + 1) * a) + ((((x |^ 4) + x) + 0) * b)) + (((c * (x |^ 3)) + (c * (x ^2))) + (0 * c)) by A2
.= ((((x |^ 5) + (1 |^ 5)) * a) + (((x |^ (3 + 1)) + x) * b)) + (((x |^ 3) + (x ^2)) * c)
.= ((((x |^ 5) + (1 |^ 5)) * a) + ((((x |^ 3) * x) + x) * b)) + (((x |^ (2 + 1)) + (x ^2)) * c) by NEWTON:6
.= ((((x |^ 5) + (1 |^ 5)) * a) + (((((x |^ 3) + 1) + 0) * x) * b)) + ((((x * (x |^ (1 + 1))) + (1 * (x ^2))) + (0 * (x ^2))) * c) by NEWTON:6
.= ((((x |^ 5) + (1 |^ 5)) * a) + (((((x |^ 3) + 1) + 0) * x) * b)) + ((((x * ((x |^ 1) * x)) + (1 * (x ^2))) + (0 * (x ^2))) * c) by NEWTON:6
.= ((((x |^ 5) + (1 |^ 5)) * a) + (((((x |^ 3) + 1) + 0) * x) * b)) + ((((x * (x ^2)) + (1 * (x ^2))) + (0 * (x ^2))) * c)
.= ((((x + 1) * (((((x |^ 4) - ((x |^ 3) * 1)) + ((x |^ 2) * (1 |^ 2))) - (x * (1 |^ 3))) + (1 |^ 4))) * a) + ((((x |^ 3) + 1) * x) * b)) + ((((x + 1) + 0) * (x ^2)) * c) by Th11
.= ((((x + 1) * (((((x |^ 4) - (x |^ 3)) + ((x |^ 2) * 1)) - (x * (1 |^ 3))) + (1 |^ 4))) * a) + ((((x |^ 3) + 1) * x) * b)) + ((((x + 1) + 0) * (x ^2)) * c)
.= ((((x + 1) * (((((x |^ 4) - (x |^ 3)) + (x |^ 2)) - (x * 1)) + (1 |^ 4))) * a) + ((((x |^ 3) + 1) * x) * b)) + ((((x + 1) + 0) * (x ^2)) * c)
.= ((((x + 1) * (((((x |^ 4) - (x |^ 3)) + (x |^ 2)) - x) + 1)) * a) + ((((x |^ 3) + 1) * x) * b)) + ((((x + 1) + 0) * (x ^2)) * c)
.= ((((x + 1) * (((((x |^ 4) - (x |^ 3)) + (x |^ 2)) - x) + 1)) * a) + ((((x |^ 3) + (1 |^ 3)) * x) * b)) + (((x + 1) * (x ^2)) * c)
.= ((((x + 1) * (((((x |^ 4) - (x |^ 3)) + (x |^ 2)) - x) + 1)) * a) + ((((x + 1) * (((x ^2) - (x * 1)) + (1 ^2))) * x) * b)) + (((x + 1) * (x ^2)) * c) by Th11
.= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + (((((x * x) * x) * b) - ((x * x) * b)) + (b * x))) + ((x * x) * c)) * (x + 1)
.= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((((x |^ 1) * x) * x) * b) - ((x * x) * b)) + (b * x))) + ((x * x) * c)) * (x + 1)
.= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((((x |^ 1) * x) * x) * b) - ((x * x) * b)) + (b * x))) + (((x |^ 1) * x) * c)) * (x + 1)
.= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((((x |^ 1) * x) * x) * b) - ((x * x) * b)) + (b * x))) + ((x |^ (1 + 1)) * c)) * (x + 1) by NEWTON:6
.= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + (((((x |^ (1 + 1)) * x) * b) - ((x * x) * b)) + (b * x))) + ((x |^ 2) * c)) * (x + 1) by NEWTON:6
.= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((x |^ (2 + 1)) * b) - ((x * x) * b)) + (b * x))) + ((x |^ 2) * c)) * (x + 1) by NEWTON:6
.= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((x |^ 3) * b) - (((x |^ 1) * x) * b)) + (b * x))) + ((x |^ 2) * c)) * (x + 1)
.= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((x |^ 3) * b) - ((x |^ (1 + 1)) * b)) + (b * x))) + ((x |^ 2) * c)) * (x + 1) by NEWTON:6
.= (((((a * (x |^ 4)) - ((a - b) * (x |^ 3))) + (((a + c) - b) * (x |^ 2))) - ((a - b) * x)) + a) * (x + 1) ;

per cases by A5;

case x + 1 = 0 ; :: thesis:

hence ( x = - 1 or x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) ; :: thesis:

end;

case A6: ((((a * (x |^ 4)) - ((a - b) * (x |^ 3))) + (((a + c) - b) * (x |^ 2))) - ((a - b) * x)) + a = 0 ; :: thesis:

set y = x + (1 / x);
0 = ((((a * (x |^ 4)) + (((- a) + b) * (x |^ 3))) + (((a + c) - b) * (x |^ (1 + 1)))) + (((- a) + b) * x)) + a by A6
.= ((((a * (x |^ 4)) + (((- a) + b) * (x |^ 3))) + (((a + c) - b) * ((x |^ 1) * x))) + (((- a) + b) * x)) + a by NEWTON:6
.= ((((a * (x |^ 4)) + (((- a) + b) * (x |^ 3))) + (((a + c) - b) * (x ^2))) + (((- a) + b) * x)) + a ;
then A7: Polynom (a,((- a) + b),((a + c) - b),((- a) + b),a,x) = 0 by POLYEQ_2:def 1;
( x + (1 / x) = x + (1 / x) & y1 = ((- ((- a) + b)) + (sqrt (((((- a) + b) ^2) - ((4 * a) * ((a + c) - b))) + (8 * (a ^2))))) / (2 * a) ) by A3;
hence ( x = - 1 or x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) by A1, A4, A7, POLYEQ_2:3; :: thesis:

end;