let F be Field; :: thesis: for E being F -algebraic FieldExtension of F
for A being AlgebraicClosure of E holds A is AlgebraicClosure of F
let E be F -algebraic FieldExtension of F; :: thesis: for A being AlgebraicClosure of E holds A is AlgebraicClosure of F
let A be AlgebraicClosure of E; :: thesis: A is AlgebraicClosure of F
reconsider B = A as FieldExtension of F ;
B is F -algebraic by FIELD_7:39;
hence A is AlgebraicClosure of F by defAC; :: thesis: verum