let z, s1, s2, a2, a1, a0, a3, s3, s4 be complex number ; :: 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 A1: ( 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 ) )
A2: (((z - s1) * (z - s2)) * (z - s3)) * (z - s4) = ((((((z * z) * z) * z) + (((a3 * z) * z) * z)) + ((a2 * z) * z)) + (a1 * z)) + a0 by A1
.= ((((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 A3: ( ((z - s1) * (z - s2)) * (z - s3) = 0 or z - s4 = 0 ) by A2;
assume ( not z = s1 & not z = s2 & not z = s3 ) ; :: thesis: z = s4
then ( z - s1 <> 0 & z - s2 <> 0 & z - s3 <> 0 ) ;
hence z = s4 by A3; :: 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 A2; :: thesis: verum