theorem pr0: :: FIELD_6:24

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 p = q holds
NormPolynomial p = NormPolynomial q