let z, a0, a1, a2, s1, s2, s3 be Complex; :: thesis: ( a2 = - ((s1 + s2) + s3) & a1 = ((s1 * s2) + (s1 * s3)) + (s2 * s3) & a0 = - ((s1 * s2) * s3) implies ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = s1 or z = s2 or z = s3 ) ) )
assume ( a2 = - ((s1 + s2) + s3) & a1 = ((s1 * s2) + (s1 * s3)) + (s2 * s3) & a0 = - ((s1 * s2) * s3) ) ; :: thesis: ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = s1 or z = s2 or z = s3 ) )
then A1: ((z - s1) * (z - s2)) * (z - s3) = ((((z * z) * z) + ((a2 * z) * z)) + (a1 * z)) + a0
.= (((z |^ 3) + (a2 * (z * z))) + (a1 * z)) + a0 by Th2
.= (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 by Th1 ;

hereby :: thesis: ( ( z = s1 or z = s2 or z = s3 ) implies (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 )

assume (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 ; :: thesis: ( not z = s1 & not z = s2 implies z = s3 )
then A2: ( (z - s1) * (z - s2) = 0 or z - s3 = 0 ) by A1;
assume ( not z = s1 & not z = s2 ) ; :: thesis: z = s3
then ( z - s1 <> 0 & z - s2 <> 0 ) ;
hence z = s3 by A2; :: thesis: verum

end;

assume ( z = s1 or z = s2 or z = s3 ) ; :: thesis: (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0
hence (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 by A1; :: thesis: verum