let x be real number ; :: thesis: for b, c being complex number st b <> 0 & ( for x being real number holds Polynom 0 ,b,c,x = 0 ) holds
x = - (c / b)
let b, c be complex number ; :: thesis: ( b <> 0 & ( for x being real number holds Polynom 0 ,b,c,x = 0 ) implies x = - (c / b) )
assume A1: b <> 0 ; :: thesis: ( ex x being real number st not Polynom 0 ,b,c,x = 0 or x = - (c / b) )
assume A2: for x being real number holds Polynom 0 ,b,c,x = 0 ; :: thesis: x = - (c / b)
set y = x;
Polynom 0 ,b,c,x = 0 by A2;
then x = (- c) / b by A1, XCMPLX_1:90
.= ((- 1) * c) * (b " ) by XCMPLX_0:def 9
.= (- 1) * (c * (b " ))
.= (- 1) * (c / b) by XCMPLX_0:def 9 ;
hence x = - (c / b) ; :: thesis: verum