let x, a, b be Real; :: thesis: ( a <> 0 & Polynom (a,b,0,x) = 0 & not x = 0 implies x = - (b / a) )

assume that

A1: a <> 0 and

A2: Polynom (a,b,0,x) = 0 ; :: thesis: ( x = 0 or x = - (b / a) )

((a * (x ^2)) + (b * x)) + 0 = 0 by A2, POLYEQ_1:def 2;

then (((a * x) + b) + 0) * x = 0 ;

then ( ((a * x) + b) + (- b) = 0 + (- b) or x = 0 ) by XCMPLX_1:6;

then ( x = (- b) / a or x = 0 ) by A1, XCMPLX_1:89;

hence ( x = 0 or x = - (b / a) ) by XCMPLX_1:187; :: thesis: verum

assume that

A1: a <> 0 and

A2: Polynom (a,b,0,x) = 0 ; :: thesis: ( x = 0 or x = - (b / a) )

((a * (x ^2)) + (b * x)) + 0 = 0 by A2, POLYEQ_1:def 2;

then (((a * x) + b) + 0) * x = 0 ;

then ( ((a * x) + b) + (- b) = 0 + (- b) or x = 0 ) by XCMPLX_1:6;

then ( x = (- b) / a or x = 0 ) by A1, XCMPLX_1:89;

hence ( x = 0 or x = - (b / a) ) by XCMPLX_1:187; :: thesis: verum