A: 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 A, FIELD_6:17;
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