let z, z1, z2 be Complex; :: thesis: ( z1 <> 0 & Polynom (z1,z2,0,z) = 0 & not z = - (z2 / z1) implies z = 0 )
assume that
A1: z1 <> 0 and
A2: Polynom (z1,z2,0,z) = 0 ; :: thesis: ( z = - (z2 / z1) or z = 0 )
0 = ((z1 * z) + z2) * z by A2;
then ( Polynom (z1,z2,z) = 0 or z = 0 ) ;
hence ( z = - (z2 / z1) or z = 0 ) by A1, Th16; :: thesis: verum