theorem ll: :: FIELD_15:15

for F being Field
for a being Element of F
for p being Polynomial of F
for E being FieldExtension of F
for b being Element of E
for q being Polynomial of E st a = b & p = q holds
a * p = b * q