let a, c, x be Real; :: thesis: ( a <> 0 & c / a < 0 & Polynom (a,0,c,0,x) = 0 & not x = 0 & not x = sqrt (- (c / a)) implies x = - (sqrt (- (c / a))) )
assume that
A1: a <> 0 and
A2: c / a < 0 ; :: thesis: ( not Polynom (a,0,c,0,x) = 0 or x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )
x |^ 3 = x |^ (2 + 1) ;
then x |^ 3 = (x |^ (1 + 1)) * x by NEWTON:6;
then A3: x |^ 3 = ((x |^ 1) * x) * x by NEWTON:6;
A4: x |^ 3 = (x ^2) * x by A3;
assume Polynom (a,0,c,0,x) = 0 ; :: thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )
then ((a * (x ^2)) + c) * x = 0 by A4;
then A5: ( x = 0 or (a * (x ^2)) + c = 0 ) by XCMPLX_1:6;

now :: thesis: ( ( x > 0 & ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ) or ( x < 0 & ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ) or ( x = 0 & ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ) )

per cases ( x > 0 or x < 0 or x = 0 ) by XXREAL_0:1;

case A6: x > 0 ; :: thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )

x |^ 2 = x |^ (1 + 1) ;
then x |^ 2 = (x |^ 1) * x by NEWTON:6;
then x |^ 2 = (x to_power 1) * x by POWER:41;
then A7: x |^ 2 = x * x by POWER:25;
A8: - (c / a) > 0 by A2, XREAL_1:58;
x ^2 = (- c) / a by A1, A5, A6, XCMPLX_1:89;
then x ^2 = (- c) * (a ") by XCMPLX_0:def 9;
then x ^2 = - (c * (a ")) ;
then x ^2 = - (c / a) by XCMPLX_0:def 9;
then x = 2 -Root (- (c / a)) by A6, A8, A7, PREPOWER:def 2;
hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) by A8, PREPOWER:32; :: thesis: verum

end;

case A9: x < 0 ; :: thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )

(- x) |^ 2 = (- x) |^ (1 + 1) ;
then (- x) |^ 2 = ((- x) |^ 1) * (- x) by NEWTON:6;
then (- x) |^ 2 = ((- x) to_power 1) * (- x) by POWER:41;
then A10: (- x) |^ 2 = (- x) * (- x) by POWER:25;
x ^2 = (- c) / a by A1, A5, A9, XCMPLX_1:89;
then x ^2 = (- c) * (a ") by XCMPLX_0:def 9;
then x ^2 = - (c * (a ")) ;
then A11: (- x) ^2 = - (c / a) by XCMPLX_0:def 9;
A12: - (c / a) > 0 by A2, XREAL_1:58;
- x > 0 by A9, XREAL_1:58;
then - x = 2 -Root (- (c / a)) by A11, A12, A10, PREPOWER:def 2;
then - x = sqrt (- (c / a)) by A12, PREPOWER:32;
hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ; :: thesis: verum

end;

case x = 0 ; :: thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )

hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ; :: thesis: verum

end;

end;

end;

hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ; :: thesis: verum