theorem Th14: :: POLYEQ_5:14

for z, a0, a1, a2, s1, s2, s3 being Complex st a2 = - ((s1 + s2) + s3) & a1 = ((s1 * s2) + (s1 * s3)) + (s2 * s3) & a0 = - ((s1 * s2) * s3) holds
( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = s1 or z = s2 or z = s3 ) )