let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L holds
( deg p = - 1 iff p = 0_. L )
let p be Polynomial of L; :: thesis: ( deg p = - 1 iff p = 0_. L )

now :: thesis: ( p = 0_. L implies deg p = - 1 )

assume p = 0_. L ; :: thesis: deg p = - 1
then len p = 0 by POLYNOM4:3;
hence deg p = - 1 ; :: thesis: verum

end;

hence ( deg p = - 1 iff p = 0_. L ) by POLYNOM4:5; :: thesis: verum