let a, b, c, a9, b9, c9 be Complex; :: thesis: ( ( for x being Real holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x) ) implies ( a = a9 & b = b9 & c = c9 ) )

assume A1: for x being Real holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x) ; :: thesis: ( a = a9 & b = b9 & c = c9 )

then A2: Polynom (a,b,c,(- 1)) = Polynom (a9,b9,c9,(- 1)) ;

( Polynom (a,b,c,0) = Polynom (a9,b9,c9,0) & Polynom (a,b,c,1) = Polynom (a9,b9,c9,1) ) by A1;

hence ( a = a9 & b = b9 & c = c9 ) by A2; :: thesis: verum

assume A1: for x being Real holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x) ; :: thesis: ( a = a9 & b = b9 & c = c9 )

then A2: Polynom (a,b,c,(- 1)) = Polynom (a9,b9,c9,(- 1)) ;

( Polynom (a,b,c,0) = Polynom (a9,b9,c9,0) & Polynom (a,b,c,1) = Polynom (a9,b9,c9,1) ) by A1;

hence ( a = a9 & b = b9 & c = c9 ) by A2; :: thesis: verum