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