theorem co: :: FIELD_14:22

for F being Field
for E being FieldExtension of F
for p being Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring E) st q = p holds
Coeff q = Coeff p