let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L st deg p <> - 1 holds
p . (deg p) <> 0. L
let p be Polynomial of L; :: thesis: ( deg p <> - 1 implies p . (deg p) <> 0. L )
assume deg p <> - 1 ; :: thesis: p . (deg p) <> 0. L
then len p <> 0 ;
hence p . (deg p) <> 0. L by Lm6; :: thesis: verum