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

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