reconsider n = deg (MinPoly (a,F)) as Element of NAT ;
deffunc H₁( Nat) -> Element of the carrier of E = a |^ F;
defpred S₁[ Nat] means F < n;
D: { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } is finite from FINSEQ_1:sch 6();

E: now :: thesis: for o being object st o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } holds
o in Base a

let o be object ; :: thesis: ( o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } implies o in Base a )
assume o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } ; :: thesis: o in Base a
then consider i being Nat such that
E1: ( o = a |^ i & i <= n & i < n ) ;
i is Element of NAT by ORDINAL1:def 12;
hence o in Base a by E1; :: thesis: verum

end;

now :: thesis: for o being object st o in Base a holds
o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) }

let o be object ; :: thesis: ( o in Base a implies o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } )
assume o in Base a ; :: thesis: o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) }
then consider i being Element of NAT such that
E1: ( o = a |^ i & i < n ) ;
thus o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } by E1; :: thesis: verum

end;

hence Base a is finite by D, E, TARSKI:2; :: thesis: verum