theorem lemma7b: :: FIELD_7:15

for F being Field
for p being Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for q being Element of the carrier of (Polynom-Ring E) st q = p holds
for U being b₃ -extending FieldExtension of F
for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a)