let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L holds
( deg p is Element of NAT iff p <> 0_. L )
let p be Polynomial of L; :: thesis: ( deg p is Element of NAT iff p <> 0_. L )

now :: thesis: ( p <> 0_. L implies deg p is Element of NAT )

assume p <> 0_. L ; :: thesis: deg p is Element of NAT
then len p <> 0 by POLYNOM4:5;
then (len p) + 1 > 0 + 1 by XREAL_1:6;
then len p >= 1 by NAT_1:13;
then (len p) - 1 is Element of NAT by INT_1:3;
hence deg p is Element of NAT by HURWITZ:def 2; :: thesis: verum

end;

hence ( deg p is Element of NAT iff p <> 0_. L ) by HURWITZ:20; :: thesis: verum