theorem Th12: :: POLYEQ_1:12

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