A: FAdj (F,{a,b}) 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,b} is Subset of (FAdj (F,{a,b})) by FIELD_6:35;
a in {a,b} by TARSKI:def 2;
then reconsider a1 = a as Element of the carrier of (FAdj (F,{a,b})) by B;
b in {a,b} by TARSKI:def 2;
then reconsider b1 = b as Element of the carrier of (FAdj (F,{a,b})) by B;
a * b = a1 * b1 by A, FIELD_6:16;
then reconsider c = a * b as FAdj (F,{a,b}) -membered Element of E1 by defmem;
@ ((@ ((FAdj (F,{a,b})),c)),E1) is F -algebraic ;
hence a * b is F -algebraic ; :: thesis: verum