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 )

( 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 )

hence
( deg p is Element of NAT iff p <> 0_. L )
by HURWITZ:20; :: thesis: verumassume
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;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