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