for F being Field
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