let b, c be Real; :: thesis: for z being Element of COMPLEX st b <> 0 & ( for z being Element of COMPLEX holds Polynom 0 ,b,c,z = 0 ) holds
z = - (c / b)
let z be Element of COMPLEX ; :: thesis: ( b <> 0 & ( for z being Element of COMPLEX holds Polynom 0 ,b,c,z = 0 ) implies z = - (c / b) )
A1: 0 = 0 + (0 * <i> ) ;
assume A2: b <> 0 ; :: thesis: ( ex z being Element of COMPLEX st not Polynom 0 ,b,c,z = 0 or z = - (c / b) )
assume A3: for z being Element of COMPLEX holds Polynom 0 ,b,c,z = 0 ; :: thesis: z = - (c / b)

now

let z1 be Element of COMPLEX ; :: thesis: z1 = - (c / b)
Polynom 0 ,b,c,z1 = 0 by A3;
then (b * ((Re z1) + ((Im z1) * <i> ))) + c = 0 by COMPLEX1:29;
then A4: (((b * (Re z1)) - 0 ) + c) + (((b * (Im z1)) + 0 ) * <i> ) = 0 + (0 * <i> ) ;
then ((b * (Re z1)) - 0 ) + c = Re 0 by COMPLEX1:28;
then ((b * (Re z1)) - 0 ) + c = 0 by A1, COMPLEX1:28;
then A5: Re z1 = (- c) / b by A2, XCMPLX_1:90;
b * (Im z1) = Im 0 by A4, COMPLEX1:28;
then Im z1 = 0 by A1, A2, COMPLEX1:28;
then z1 = (- (c / b)) + (0 * <i> ) by A5, COMPLEX1:29;
hence z1 = - (c / b) ; :: thesis: verum

end;

hence z = - (c / b) ; :: thesis: verum