let a, b, c, d, a9, b9, c9, d9 be Real; :: thesis: ( ( for z being complex number holds Polynom a,b,c,d,z = Polynom a9,b9,c9,d9,z ) implies ( a = a9 & b = b9 & c = c9 & d = d9 ) )
assume A1: for z being complex number holds Polynom a,b,c,d,z = Polynom a9,b9,c9,d9,z ; :: thesis: ( a = a9 & b = b9 & c = c9 & d = d9 )
then A2: Polynom a,b,c,d,0 = Polynom a9,b9,c9,d9,0 ;
A3: ( Polynom a,b,c,d,1 = Polynom a9,b9,c9,d9,1 & Polynom a,b,c,d,(- 1) = Polynom a9,b9,c9,d9,(- 1) ) by A1;
A4: Polynom a,b,c,d,2 = Polynom a9,b9,c9,d9,2 by A1;
hence a = a9 by A2, A3; :: thesis: ( b = b9 & c = c9 & d = d9 )
thus b = b9 by A2, A3; :: thesis: ( c = c9 & d = d9 )
thus c = c9 by A2, A3, A4; :: thesis: d = d9
thus d = d9 by A2; :: thesis: verum