let F be Field; :: thesis: for E being FieldExtension of F
for p being non zero Polynomial of E st Coeff p c= the carrier of F holds
p is non zero Polynomial of F
let E be FieldExtension of F; :: thesis: for p being non zero Polynomial of E st Coeff p c= the carrier of F holds
p is non zero Polynomial of F
let p be non zero Polynomial of E; :: thesis: ( Coeff p c= the carrier of F implies p is non zero Polynomial of F )
assume Coeff p c= the carrier of F ; :: thesis: p is non zero Polynomial of F
then reconsider q = p as Polynomial of F by cof1;
p <> 0_. E ;
then q <> 0_. F by FIELD_4:12;
hence p is non zero Polynomial of F by UPROOTS:def 5; :: thesis: verum