let F be Field; :: thesis: for E being F -algebraic FieldExtension of F holds F_Alg E == E
let E be F -algebraic FieldExtension of F; :: thesis: F_Alg E == E
A: E is FieldExtension of F_Alg E by ee;
F_Alg E is FieldExtension of E by t2;
hence F_Alg E == E by A, FIELD_4:7; :: thesis: verum