let x be Real; :: thesis: for b, c being Complex st b <> 0 & ( for x being Real holds Polynom (0,b,c,x) = 0 ) holds
x = - (c / b)
let b, c be Complex; :: thesis: ( b <> 0 & ( for x being Real holds Polynom (0,b,c,x) = 0 ) implies x = - (c / b) )
assume A1: b <> 0 ; :: thesis: ( ex x being Real st not Polynom (0,b,c,x) = 0 or x = - (c / b) )
set y = x;
assume for x being Real holds Polynom (0,b,c,x) = 0 ; :: thesis: x = - (c / b)
then Polynom (0,b,c,x) = 0 ;
then x = (- c) / b by A1, XCMPLX_1:89
.= ((- 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