theorem Th4: :: POLYEQ_1:4

for a, b, c, a9, b9, c9 being Complex st ( for x being Real holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x) ) holds
( a = a9 & b = b9 & c = c9 )