let F be Field; :: thesis: for E1, E2 being FieldExtension of F st E1 == E2 holds
{ f where f is Automorphism of E1 : verum } = { f where f is Automorphism of E2 : verum }
let E1, E2 be FieldExtension of F; :: thesis: ( E1 == E2 implies { f where f is Automorphism of E1 : verum } = { f where f is Automorphism of E2 : verum } )
assume AS: E1 == E2 ; :: thesis: { f where f is Automorphism of E1 : verum } = { f where f is Automorphism of E2 : verum }

A: now :: thesis: for o being object st o in { f where f is Automorphism of E1 : verum } holds
o in { f where f is Automorphism of E2 : verum }

let o be object ; :: thesis: ( o in { f where f is Automorphism of E1 : verum } implies o in { f where f is Automorphism of E2 : verum } )
assume o in { f where f is Automorphism of E1 : verum } ; :: thesis: o in { f where f is Automorphism of E2 : verum }
then consider g being Automorphism of E1 such that
B: o = g ;
g is Automorphism of E2 by AS, FAutEQ1;
hence o in { f where f is Automorphism of E2 : verum } by B; :: thesis: verum

end;

now :: thesis: for o being object st o in { f where f is Automorphism of E2 : verum } holds
o in { f where f is Automorphism of E1 : verum }

let o be object ; :: thesis: ( o in { f where f is Automorphism of E2 : verum } implies o in { f where f is Automorphism of E1 : verum } )
assume o in { f where f is Automorphism of E2 : verum } ; :: thesis: o in { f where f is Automorphism of E1 : verum }
then consider g being Automorphism of E2 such that
B: o = g ;
g is Automorphism of E1 by AS, FAutEQ1;
hence o in { f where f is Automorphism of E1 : verum } by B; :: thesis: verum

end;

hence { f where f is Automorphism of E1 : verum } = { f where f is Automorphism of E2 : verum } by A, TARSKI:2; :: thesis: verum