theorem :: POLYEQ_1:13

for a, b, c, d, x1, x2, x3 being Real st a <> 0 & ( for x being Real holds Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) ) holds
( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) )