let F be Field; :: thesis: for p being Ppoly of F holds p splits_in F
let p be Ppoly of F; :: thesis: p splits_in F
p = (1. F) * p ;
hence p splits_in F by FIELD_4:def 5; :: thesis: verum