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

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

assume ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 ; :: thesis: ( not z = s1 & not z = s2 & not z = s3 implies z = s4 )
then A2: ( ((z - s1) * (z - s2)) * (z - s3) = 0 or z - s4 = 0 ) by A1;
assume that
A3: ( not z = s1 & not z = s2 ) and
A4: not z = s3 ; :: thesis: z = s4
A5: z - s3 <> 0 by A4;
( z - s1 <> 0 & z - s2 <> 0 ) by A3;
hence z = s4 by A2, A5; :: thesis: verum

end;

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