let a, b, c, a9, b9, c9 be complex number ; :: thesis: ( ( for x being real number holds Polynom a,b,c,x = Polynom a9,b9,c9,x ) implies ( a = a9 & b = b9 & c = c9 ) )
assume A1: for x being real number holds Polynom a,b,c,x = Polynom a9,b9,c9,x ; :: thesis: ( 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; :: thesis: verum