let F1, F2 be Field; :: thesis: for E being AlgebraicClosure of F1 st F1 == F2 holds
E is AlgebraicClosure of F2
let E be AlgebraicClosure of F1; :: thesis: ( F1 == F2 implies E is AlgebraicClosure of F2 )
assume F1 == F2 ; :: thesis: E is AlgebraicClosure of F2
then reconsider E3 = E as F2 -algebraic FieldExtension of F2 by lift5;
E3 is algebraic-closed ;
hence E is AlgebraicClosure of F2 by defAC; :: thesis: verum