theorem :: FIELD_8:24

for F being Field
for E being FieldExtension of F
for p being Ppoly of F holds p is Ppoly of E by lemmapp;