let z1, z2, z3, s1, s2, s3 be Complex; :: thesis: ( ( for z being Complex holds Polynom (z1,z2,z3,z) = Polynom (s1,s2,s3,z) ) implies ( z1 = s1 & z2 = s2 & z3 = s3 ) )
assume A1: for z being 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 4; :: thesis: verum