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,(- 1) = Polynom a',b',c',(- 1) ;
( Polynom a,b,c,0 = Polynom a',b',c',0 & Polynom a,b,c,1 = Polynom a',b',c',1 ) by A1;
hence ( a = a' & b = b' & c = c' ) by A2; :: thesis: verum