let a1, a2, a3, a4, a5, x, x1, x2, x3, x4 be Real; :: thesis: ( a1 <> 0 & ( for x being Real 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 ^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) )
assume A1: a1 <> 0 ; :: thesis: ( ex x being Real 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 ^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) )
set z = (((x - x1) * (x - x2)) * (x - x3)) * (x - x4);
set w = ((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5;
assume for x being Real holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ; :: thesis: (((((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)
then Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ;
then (((((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1) * a1) - (((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)) * a1) = (((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)) * a1) - (((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)) * a1) by A1, XCMPLX_1:87;
then (((((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1) - ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4))) * a1 = 0 ;
then ((((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1) + (- ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4))) = 0 - 0 by A1, XCMPLX_1:6;
hence (((((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) ; :: thesis: verum