let a, b, c, d, x1, x2, x3 be Real; :: thesis: ( a <> 0 & ( for x being Real holds Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) ) implies ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) ) )
assume A1: a <> 0 ; :: thesis: ( ex x being Real st not Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) or ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) ) )
set t3 = d / a;
set t2 = c / a;
set t1 = b / a;
set d9 = - ((x1 * x2) * x3);
set c9 = ((x1 * x2) + (x2 * x3)) + (x1 * x3);
set b9 = - ((x1 + x2) + x3);
assume A2: for x being Real holds Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) ; :: thesis: ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) )

now :: thesis: for x being Real holds Polynom (1,(b / a),(c / a),(d / a),x) = Polynom (1,(- ((x1 + x2) + x3)),(((x1 * x2) + (x2 * x3)) + (x1 * x3)),(- ((x1 * x2) * x3)),x)

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

end;

hence ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) ) by Th12; :: thesis: verum