let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E holds { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } is finite
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E holds { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } is finite
let a be F -algebraic Element of E; :: thesis: { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } is finite
set M = { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } ;
set R = Roots ((FAdj (F,{a})),(MinPoly (a,F)));
( a in {a} & {a} is Subset of (FAdj (F,{a})) ) by TARSKI:def 1, FIELD_6:35;
then reconsider a1 = a as Element of (FAdj (F,{a})) ;
D: E is FAdj (F,{a}) -extending by FIELD_4:7;
0. (FAdj (F,{a})) = 0. E by FIELD_6:def 6
.= Ext_eval ((MinPoly (a,F)),a) by FIELD_6:52
.= Ext_eval ((MinPoly (a,F)),a1) by D, FIELD_6:11 ;
then a1 is_a_root_of MinPoly (a,F), FAdj (F,{a}) by FIELD_4:def 2;
then a1 in { b where b is Element of (FAdj (F,{a})) : b is_a_root_of MinPoly (a,F), FAdj (F,{a}) } ;
then I: Roots ((FAdj (F,{a})),(MinPoly (a,F))) <> {} by FIELD_4:def 4;
defpred S₁[ object , object ] means ex g being F -fixing Automorphism of (FAdj (F,{a})) st
( $1 = g & $2 = g . a );

B: now :: thesis: for x being object st x in { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } holds
ex y being object st
( y in Roots ((FAdj (F,{a})),(MinPoly (a,F))) & S₁[x,y] )

let x be object ; :: thesis: ( x in { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } implies ex y being object st
( y in Roots ((FAdj (F,{a})),(MinPoly (a,F))) & S₁[x,y] ) )
assume x in { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } ; :: thesis: ex y being object st
( y in Roots ((FAdj (F,{a})),(MinPoly (a,F))) & S₁[x,y] )
then consider g being F -fixing Automorphism of (FAdj (F,{a})) such that
B1: x = g ;
g . a in Roots ((FAdj (F,{a})),(MinPoly (a,F))) by ID2a;
hence ex y being object st
( y in Roots ((FAdj (F,{a})),(MinPoly (a,F))) & S₁[x,y] ) by B1; :: thesis: verum

end;

consider h being Function of { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } ,(Roots ((FAdj (F,{a})),(MinPoly (a,F)))) such that
A: for o being object st o in { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } holds
S₁[o,h . o] from FUNCT_2:sch 1(B);

now :: thesis: for x1, x2 being object st x1 in { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } & x2 in { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } & h . x1 = h . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } & x2 in { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } & h . x1 = h . x2 implies x1 = x2 )
assume A0: ( x1 in { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } & x2 in { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } & h . x1 = h . x2 ) ; :: thesis: x1 = x2
then consider g1 being F -fixing Automorphism of (FAdj (F,{a})) such that
A1: ( x1 = g1 & h . x1 = g1 . a ) by A;
consider g2 being F -fixing Automorphism of (FAdj (F,{a})) such that
A2: ( x2 = g2 & h . x2 = g2 . a ) by A, A0;
thus x1 = x2 by A0, A1, A2, ID; :: thesis: verum

end;

then B: h is one-to-one by I, FUNCT_2:19;
rng h c= Roots ((FAdj (F,{a})),(MinPoly (a,F))) by RELAT_1:def 19;
then dom h is finite by B, CARD_1:59;
hence { f where f is F -fixing Automorphism of (FAdj (F,{a})) : verum } is finite by I, FUNCT_2:def 1; :: thesis: verum