let z1, z2, z be Element of 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, Th24; :: thesis: verum