let z, z1, z2 be Complex; :: thesis: ( z1 <> 0 & Polynom (z1,z2,z) = 0 implies z = - (z2 / z1) )
assume ( z1 <> 0 & Polynom (z1,z2,z) = 0 ) ; :: thesis: z = - (z2 / z1)
then z = (- z2) * (z1 ") by XCMPLX_1:203;
hence z = - (z2 / z1) ; :: thesis: verum