let a, b, x be Complex; :: thesis: ( a <> 0 & Polynom (a,b,x) = 0 implies x = - (b / a) )
assume that
A1: a <> 0 and
A2: Polynom (a,b,x) = 0 ; :: thesis: x = - (b / a)
(a ") * (- b) = (a ") * (a * x) by A2
.= ((a ") * a) * x ;
then 1 * x = (a ") * (- b) by A1, XCMPLX_0:def 7;
then x = - ((a ") * b) ;
hence x = - (b / a) by XCMPLX_0:def 9; :: thesis: verum