let a1, a2, a3, a4, a5, x, x1, x2, x3, x4 be real number ; ( a1 <> 0 & ( for x being real number holds Polynom a1,a2,a3,a4,a5,x = Four0 a1,x1,x2,x3,x4,x ) implies (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2 ))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) )
assume A1:
a1 <> 0
; ( ex x being real number st not Polynom a1,a2,a3,a4,a5,x = Four0 a1,x1,x2,x3,x4,x or (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2 ))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) )
set w = ((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5;
assume
for x being real number holds Polynom a1,a2,a3,a4,a5,x = Four0 a1,x1,x2,x3,x4,x
; (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2 ))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4)
then
(((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5) / a1 = (((((x ^2 ) * (x ^2 )) - (((x1 + x2) + x3) * ((x ^2 ) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2 ))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4)
by A1, Th10;
then
(((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5) / a1 = (((((x ^2 ) * (x ^2 )) - ((((x1 + x2) + x3) + x4) * ((x ^2 ) * x))) + (((((x1 * x3) + (x2 * x3)) + (x1 * x2)) + (((x2 * x4) + (x1 * x4)) + (x3 * x4))) * (x ^2 ))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + (- (- ((x1 * x3) * x4)))) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4)
;
then
(((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * ((x ^2 ) * x))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2 ))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4)
by Th4;
hence
(((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2 ))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4)
by Th4; verum