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

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