let a, b, c, a', b', c' be complex number ; :: thesis: ( ( for x being real number holds Polynom a,b,c,x = Polynom a',b',c',x ) implies ( a = a' & b = b' & c = c' ) )
assume A1: for x being real number holds Polynom a,b,c,x = Polynom a',b',c',x ; :: thesis: ( a = a' & b = b' & c = c' )
then A2: Polynom a,b,c,0 = Polynom a',b',c',0 ;
A3: Polynom a,b,c,1 = Polynom a',b',c',1 by A1;
Polynom a,b,c,(- 1) = Polynom a',b',c',(- 1) by A1;
hence ( a = a' & b = b' & c = c' ) by A2, A3; :: thesis: verum