let a, b, c, d, a9, b9, c9, d9 be Real; :: thesis: ( ( for z being Complex 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 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