let a, x be Real; :: thesis: ( a <> 0 & Polynom a,0 ,0 ,x = 0 implies x = 0 )
assume that
A1: a <> 0 and
A2: Polynom a,0 ,0 ,x = 0 ; :: thesis: x = 0
((a * (x ^2 )) + (0 * x)) + 0 = 0 by A2, POLYEQ_1:def 2;
then x ^2 = 0 by A1, XCMPLX_1:6;
hence x = 0 by XCMPLX_1:6; :: thesis: verum