for F being Field
for E being FieldExtension of F
for p being Polynomial of F st deg p < 2 holds
for a being Element of E ex y, z being b₁ -membered Element of E st Ext_eval (p,a) = y + (a * z)