set K = the FieldExtension of E;
take the FieldExtension of E ; :: thesis: the FieldExtension of E is F -extending
thus the FieldExtension of E is F -extending ; :: thesis: verum