let p be Polynomial of L; :: thesis: ( p is zero implies p is constant )
assume p is zero ; :: thesis: p is constant
then p = 0_. L by defzer;
hence p is constant ; :: thesis: verum