let x be Real; :: thesis: Polynom (1,(b / a),(c / a),(d / a),x) = Polynom (1,(- ((x1 + x2) + x3)),(((x1 * x2) + (x2 * x3)) + (x1 * x3)),(- ((x1 * x2) * x3)),x)
set t = (((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d;
set r8 = ((x - x1) * (x - x2)) * (x - x3);
x |^ 3 = x |^ (2 + 1)
.= (x |^ (1 + 1)) * x by NEWTON:6
.= ((x |^ 1) * x) * x by NEWTON:6 ;
then A3: x |^ 3 = (x * x) * x ;
Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) by A2;
then A4: ((((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d) / a = ((x - x1) * (x - x2)) * (x - x3) by A1, XCMPLX_1:89;
(a ") * ((((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d) = ((((a ") * a) * (x |^ 3)) + (((a ") * b) * (x ^2))) + ((a ") * ((c * x) + d))
.= ((1 * (x |^ 3)) + (((a ") * b) * (x ^2))) + ((((a ") * c) * x) + ((a ") * d)) by A1, XCMPLX_0:def 7
.= ((1 * (x |^ 3)) + ((b / a) * (x ^2))) + ((((a ") * c) * x) + ((a ") * d)) by XCMPLX_0:def 9
.= ((1 * (x |^ 3)) + ((b / a) * (x ^2))) + (((c / a) * x) + ((a ") * d)) by XCMPLX_0:def 9
.= ((1 * (x |^ 3)) + ((b / a) * (x ^2))) + (((c / a) * x) + (d / a)) by XCMPLX_0:def 9
.= Polynom (1,(b / a),(c / a),(d / a),x) ;
hence Polynom (1,(b / a),(c / a),(d / a),x) = Polynom (1,(- ((x1 + x2) + x3)),(((x1 * x2) + (x2 * x3)) + (x1 * x3)),(- ((x1 * x2) * x3)),x) by A4, A3, XCMPLX_0:def 9; :: thesis: verum