for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E
for x, y being Element of (FAdj (F,{a}))
for p, q being Polynomial of F st x = Ext_eval (p,a) & y = Ext_eval (q,a) holds
( x + y = Ext_eval ((p + q),a) & x * y = Ext_eval ((p *' q),a) )