let z1, z2, z3, s1, s2, s3 be Element of COMPLEX ; :: thesis: ( ( for z being Element of COMPLEX holds Polynom z1,z2,z3,z = Polynom s1,s2,s3,z ) implies ( z1 = s1 & z2 = s2 & z3 = s3 ) )
assume A1: for z being Element of COMPLEX holds Polynom z1,z2,z3,z = Polynom s1,s2,s3,z ; :: thesis: ( z1 = s1 & z2 = s2 & z3 = s3 )
then A2: Polynom z1,z2,z3,(- 1r ) = Polynom s1,s2,s3,(- 1r ) ;
( Polynom z1,z2,z3,0c = Polynom s1,s2,s3,0c & Polynom z1,z2,z3,1r = Polynom s1,s2,s3,1r ) by A1;
hence ( z1 = s1 & z2 = s2 & z3 = s3 ) by A2, COMPLEX1:def 7; :: thesis: verum