theorem divfin1: :: FIELD_14:56

for F being Field
for E being FieldExtension of F
for p being Polynomial of F
for q being Polynomial of E st q = p holds
MonicDivisors p c= MonicDivisors q