theorem lemNor1cv: :: FIELD_13:13

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