reconsider K = E as F -extending FieldExtension of F by FIELD_4:6;
take K ; :: thesis: K is F -finite
thus K is F -finite ; :: thesis: verum