let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L st 0 <= deg p holds
p is non-zero
let p be Polynomial of L; :: thesis: ( 0 <= deg p implies p is non-zero )
assume 0 <= deg p ; :: thesis: p is non-zero
then deg p <> - 1 ;
then p <> 0_. L by HURWITZ:20;
hence p is non-zero by UPROOTS:def 5; :: thesis: verum