let p be non constant Polynomial of F; :: thesis: p is with_roots
deg p > 0 by RATFUNC1:def 2;
then (len p) - 1 > 0 by HURWITZ:def 2;
then ((len p) - 1) + 1 > 0 + 1 by XREAL_1:6;
hence p is with_roots by POLYNOM5:def 9; :: thesis: verum