let L be non empty ZeroStr ; :: thesis: for p being constant Polynomial of L holds
( p = 0_. L or p = <%(p . 0)%> )
let p be constant Polynomial of L; :: thesis: ( p = 0_. L or p = <%(p . 0)%> )
deg p <= 0 by RATFUNC1:def 2;
then ((len p) - 1) + 1 <= 0 + 1 by XREAL_1:6;
hence ( p = 0_. L or p = <%(p . 0)%> ) by ALGSEQ_1:def 5; :: thesis: verum