let a, c, x be real number ; :: 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 A1: ( a <> 0 & 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))) )
assume A2: Polynom a,0 ,c,0 ,x = 0 ; :: thesis: ( 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:11;
then A3: x |^ 3 = ((x |^ 1) * x) * x by NEWTON:11;
x |^ 1 = x to_power 1 by POWER:46;
then x |^ 3 = (x ^2 ) * x by A3, POWER:30;
then ((a * (x ^2 )) + c) * x = 0 by A2;
then A4: ( x = 0 or (a * (x ^2 )) + c = 0 ) by XCMPLX_1:6;

now

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

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

then x ^2 = (- c) / a by A1, A4, XCMPLX_1:90;
then x ^2 = (- c) * (a " ) by XCMPLX_0:def 9;
then x ^2 = - (c * (a " )) ;
then A6: x ^2 = - (c / a) by XCMPLX_0:def 9;
A7: - (c / a) > 0 by A1, XREAL_1:60;
x |^ 2 = x |^ (1 + 1) ;
then x |^ 2 = (x |^ 1) * x by NEWTON:11;
then x |^ 2 = (x to_power 1) * x by POWER:46;
then x |^ 2 = x * x by POWER:30;
then x = 2 -Root (- (c / a)) by A5, A6, A7, PREPOWER:def 3;
hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) by A7, PREPOWER:41; :: thesis: verum

end;

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

then A9: - x > 0 by XREAL_1:60;
x ^2 = (- c) / a by A1, A4, A8, XCMPLX_1:90;
then x ^2 = (- c) * (a " ) by XCMPLX_0:def 9;
then x ^2 = - (c * (a " )) ;
then A10: (- x) ^2 = - (c / a) by XCMPLX_0:def 9;
A11: - (c / a) > 0 by A1, XREAL_1:60;
(- x) |^ 2 = (- x) |^ (1 + 1) ;
then (- x) |^ 2 = ((- x) |^ 1) * (- x) by NEWTON:11;
then (- x) |^ 2 = ((- x) to_power 1) * (- x) by POWER:46;
then (- x) |^ 2 = (- x) * (- x) by POWER:30;
then - x = 2 -Root (- (c / a)) by A9, A10, A11, PREPOWER:def 3;
then - x = sqrt (- (c / a)) by A11, PREPOWER:41;
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