theorem cof1: :: FIELD_7:11

for F being Field
for E being FieldExtension of F
for p being Polynomial of E st Coeff p c= the carrier of F holds
p is Polynomial of F