theorem Th9: :: POLYEQ_2:9
for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being Real st ( for x being Real holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) holds
( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 )