theorem simpA: :: FIELD_14:77

for F being 0 -characteristic Field
for E being FieldExtension of F
for a, b being b₁ -algebraic Element of E ex x being Element of F st FAdj (F,{a,b}) = FAdj (F,{(a + ((@ (x,E)) * b))})