let x, a, b be Real; ( 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
; ( 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; verum