reconsider n = deg (MinPoly (a,F)) as Element of NAT ;
deffunc H1( Nat) -> Element of the carrier of E = a |^ F;
defpred S1[ Nat] means F < n;
D: { H1(i) where i is Nat : ( i <= n & S1[i] ) } is finite from FINSEQ_1:sch 6();
E: now :: thesis: for o being object st o in { H1(i) where i is Nat : ( i <= n & S1[i] ) } holds
o in Base a
let o be object ; :: thesis: ( o in { H1(i) where i is Nat : ( i <= n & S1[i] ) } implies o in Base a )
assume o in { H1(i) where i is Nat : ( i <= n & S1[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 { H1(i) where i is Nat : ( i <= n & S1[i] ) }
let o be object ; :: thesis: ( o in Base a implies o in { H1(i) where i is Nat : ( i <= n & S1[i] ) } )
assume o in Base a ; :: thesis: o in { H1(i) where i is Nat : ( i <= n & S1[i] ) }
then consider i being Element of NAT such that
E1: ( o = a |^ i & i < n ) ;
thus o in { H1(i) where i is Nat : ( i <= n & S1[i] ) } by E1; :: thesis: verum
end;
hence Base a is finite by D, E, TARSKI:2; :: thesis: verum