reconsider aF = a as Element of F by FIELD_7:def 5;
F is Subfield of E by FIELD_4:7;
then a " = aF " by FIELD_6:18;
hence a " is F -membered by FIELD_7:def 5; :: thesis: verum