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

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