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

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

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

end;

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