let a, b, x be complex number ; :: 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