theorem pr1: :: FIELD_6:25

for F being Field
for E being FieldExtension of F
for p being Element of the carrier of (Polynom-Ring F)
for a being Element of E holds
( Ext_eval (p,a) = 0. E iff Ext_eval ((NormPolynomial p),a) = 0. E )