FAdj (F,{a}) is Subring of E by FIELD_5:12;
then reconsider E1 = E as F -extending FieldExtension of F by FIELD_4:def 1;
B: {a} is Subset of (FAdj (F,{a})) by FIELD_6:35;
a in {a} by TARSKI:def 1;
then reconsider a1 = a as Element of the carrier of (FAdj (F,{a})) by B;
a " = a1 " by FIELD_6:18;
then reconsider c = a " as FAdj (F,{a}) -membered Element of E1 by defmem;
@ ((@ ((FAdj (F,{a})),c)),E1) is F -algebraic ;
hence a " is F -algebraic ; :: thesis: verum