let a, b, c, a9, b9, c9 be Complex; ( ( for x being Real holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x) ) implies ( a = a9 & b = b9 & c = c9 ) )
assume A1:
for x being Real holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x)
; ( a = a9 & b = b9 & c = c9 )
then A2:
Polynom (a,b,c,(- 1)) = Polynom (a9,b9,c9,(- 1))
;
( Polynom (a,b,c,0) = Polynom (a9,b9,c9,0) & Polynom (a,b,c,1) = Polynom (a9,b9,c9,1) )
by A1;
hence
( a = a9 & b = b9 & c = c9 )
by A2; verum