let a, b, x be complex number ; :: thesis: ( a <> 0 & Polynom a,b,x = 0 implies x = - (b / a) )
assume A1: ( a <> 0 & Polynom a,b,x = 0 ) ; :: thesis: x = - (b / a)
then (a " ) * (- b) = (a " ) * (a * x)
.= ((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