let E be FieldExtension of F; :: thesis: ( E is F -finite implies E is F -algebraic )
assume AS: E is F -finite ; :: thesis: E is F -algebraic
then reconsider n = deg (E,F) as Element of NAT by ORDINAL1:def 12;
H: n = dim (VecSp (E,F)) by FIELD_4:def 7;

now :: thesis: for a being Element of E holds a is F -algebraic

let a be Element of E; :: thesis: b₁ is F -algebraic

per cases ( ex i, j being Element of NAT st
( i < j & j <= n & a |^ i = a |^ j ) or for i, j being Element of NAT holds
( not i < j or not j <= n or not a |^ i = a |^ j ) ) ;

suppose ex i, j being Element of NAT st
( i < j & j <= n & a |^ i = a |^ j ) ; :: thesis: b₁ is F -algebraic

then consider i, j being Element of NAT such that
U: ( i < j & j <= n & a |^ i = a |^ j ) ;
set p1 = <%(0. F),(1. F)%> `^ j;
set p2 = <%(0. F),(1. F)%> `^ i;
set p = (<%(0. F),(1. F)%> `^ j) - (<%(0. F),(1. F)%> `^ i);

now :: thesis: not (<%(0. F),(1. F)%> `^ j) - (<%(0. F),(1. F)%> `^ i) = 0_. F

assume (<%(0. F),(1. F)%> `^ j) - (<%(0. F),(1. F)%> `^ i) = 0_. F ; :: thesis: contradiction
then 0. F = ((<%(0. F),(1. F)%> `^ j) - (<%(0. F),(1. F)%> `^ i)) . j
.= ((<%(0. F),(1. F)%> `^ j) . j) - ((<%(0. F),(1. F)%> `^ i) . j) by POLYNOM3:27
.= (1. F) - ((<%(0. F),(1. F)%> `^ i) . j) by help1
.= (1. F) - (0. F) by U, help2 ;
hence contradiction ; :: thesis: verum

end;

then reconsider p = (<%(0. F),(1. F)%> `^ j) - (<%(0. F),(1. F)%> `^ i) as non zero Polynomial of F by UPROOTS:def 5;

per cases ( i = 0 or not i is zero ) ;

suppose T: i = 0 ; :: thesis: b₁ is F -algebraic

then W: a |^ i = 1_ E by BINOM:8;
Ext_eval (p,a) = (Ext_eval ((<%(0. F),(1. F)%> `^ j),a)) - (Ext_eval ((<%(0. F),(1. F)%> `^ i),a)) by FIELD_6:27
.= (Ext_eval ((<%(0. F),(1. F)%> `^ j),a)) - (Ext_eval ((1_. F),a)) by T, POLYNOM5:15
.= (Ext_eval ((<%(0. F),(1. F)%> `^ j),a)) - (1. E) by FIELD_4:23
.= (a |^ j) - (1. E) by U, FIELD_6:22
.= 0. E by W, U, RLVECT_1:15 ;
hence a is F -algebraic by FIELD_6:43; :: thesis: verum

end;

suppose T: not i is zero ; :: thesis: b₁ is F -algebraic

Ext_eval (p,a) = (Ext_eval ((<%(0. F),(1. F)%> `^ j),a)) - (Ext_eval ((<%(0. F),(1. F)%> `^ i),a)) by FIELD_6:27
.= (a |^ j) - (Ext_eval ((<%(0. F),(1. F)%> `^ i),a)) by U, FIELD_6:22
.= (a |^ j) - (a |^ i) by T, FIELD_6:22
.= 0. E by U, RLVECT_1:15 ;
hence a is F -algebraic by FIELD_6:43; :: thesis: verum

end;

end;

end;

suppose U: for i, j being Element of NAT holds
( not i < j or not j <= n or not a |^ i = a |^ j ) ; :: thesis: b₁ is F -algebraic

set M = { (a |^ i) where i is Element of NAT : i <= n } ;
set V = VecSp (E,F);
I: { (a |^ i) where i is Element of NAT : i <= n } c= the carrier of (VecSp (E,F))

proof

now :: thesis: for o being object st o in { (a |^ i) where i is Element of NAT : i <= n } holds
o in the carrier of (VecSp (E,F))

let o be object ; :: thesis: ( o in { (a |^ i) where i is Element of NAT : i <= n } implies o in the carrier of (VecSp (E,F)) )
assume o in { (a |^ i) where i is Element of NAT : i <= n } ; :: thesis: o in the carrier of (VecSp (E,F))
then consider i being Element of NAT such that
H: ( o = a |^ i & i <= n ) ;
the carrier of (VecSp (E,F)) = the carrier of E by FIELD_4:def 6;
hence o in the carrier of (VecSp (E,F)) by H; :: thesis: verum

end;

hence { (a |^ i) where i is Element of NAT : i <= n } c= the carrier of (VecSp (E,F)) ; :: thesis: verum

end;

{ (a |^ i) where i is Element of NAT : i <= n } is finite

proof

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 { (a |^ i) where i is Element of NAT : i <= n }

let o be object ; :: thesis: ( o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } implies o in { (a |^ i) where i is Element of NAT : i <= n } )
assume o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } ; :: thesis: o in { (a |^ i) where i is Element of NAT : i <= n }
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 { (a |^ i) where i is Element of NAT : i <= n } by E1; :: thesis: verum

end;

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

let o be object ; :: thesis: ( o in { (a |^ i) where i is Element of NAT : i <= n } implies o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } )
assume o in { (a |^ i) where i is Element of NAT : i <= n } ; :: 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 { (a |^ i) where i is Element of NAT : i <= n } is finite by D, E, TARSKI:2; :: thesis: verum

end;

then reconsider M = { (a |^ i) where i is Element of NAT : i <= n } as finite Subset of (VecSp (E,F)) by I;
card M = n + 1

proof

set m = n + 1;
defpred S₁[ object , object ] means ex x being Element of Seg (n + 1) ex y being Element of NAT st
( F = x & y = x - 1 & c₂ = a |^ y );
B1: for x, y1, y2 being object st x in Seg (n + 1) & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;

B2: now :: thesis: for x being object st x in Seg (n + 1) holds
ex y being object st S₁[x,y]

let x be object ; :: thesis: ( x in Seg (n + 1) implies ex y being object st S₁[x,y] )
assume x in Seg (n + 1) ; :: thesis: ex y being object st S₁[x,y]
then reconsider i = x as Element of Seg (n + 1) ;
1 <= i by FINSEQ_1:1;
then reconsider z = i - 1 as Element of NAT by INT_1:3;
thus ex y being object st S₁[x,y] :: thesis: verum

proof

take a |^ z ; :: thesis: S₁[x,a |^ z]
thus S₁[x,a |^ z] ; :: thesis: verum

end;

end;

consider f being Function such that
C: ( dom f = Seg (n + 1) & ( for x being object st x in Seg (n + 1) holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(B1, B2);

A1: now :: thesis: for o being object st o in M holds
o in rng f

let o be object ; :: thesis: ( o in M implies o in rng f )
assume o in M ; :: thesis: o in rng f
then consider i being Element of NAT such that
A2: ( o = a |^ i & i <= n ) ;
( 0 + 1 <= i + 1 & i + 1 <= n + 1 ) by A2, XREAL_1:6;
then reconsider x = i + 1 as Element of Seg (n + 1) by FINSEQ_1:1;
S₁[x,f . x] by C;
hence o in rng f by C, A2, FUNCT_1:def 3; :: thesis: verum

end;

now :: thesis: for o being object st o in rng f holds
o in M

let o be object ; :: thesis: ( o in rng f implies o in M )
assume o in rng f ; :: thesis: o in M
then consider u being object such that
A2: ( u in dom f & o = f . u ) by FUNCT_1:def 3;
S₁[u,f . u] by C, A2;
then consider x being Element of Seg (n + 1), y being Element of NAT such that
A3: ( u = x & y = x - 1 & f . x = a |^ y ) ;
( 1 <= x & x <= n + 1 ) by FINSEQ_1:1;
then y < ((n + 1) - 1) + 1 by A3, XREAL_1:9, NAT_1:13;
then y <= n by NAT_1:13;
hence o in M by A2, A3; :: thesis: verum

end;

then A: rng f = M by A1, TARSKI:2;

now :: thesis: f is one-to-one

assume not f is one-to-one ; :: thesis: contradiction
then consider x1, x2 being object such that
A1: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 & x1 <> x2 ) ;
consider n1 being Element of Seg (n + 1), y1 being Element of NAT such that
A2: ( x1 = n1 & y1 = n1 - 1 & f . x1 = a |^ y1 ) by A1, C;
consider n2 being Element of Seg (n + 1), y2 being Element of NAT such that
A3: ( x2 = n2 & y2 = n2 - 1 & f . x2 = a |^ y2 ) by A1, C;
( n1 <= n + 1 & n2 <= n + 1 ) by FINSEQ_1:1;
then A4: ( y1 < ((n + 1) - 1) + 1 & y2 < ((n + 1) - 1) + 1 ) by A3, A2, XREAL_1:9, NAT_1:13;
A5: y1 <> y2 by A1, A2, A3;
A6: ( y1 <= n & y2 <= n ) by A4, NAT_1:13;

per cases ( y1 < y2 or y1 > y2 ) by A5, XXREAL_0:1;

suppose y1 < y2 ; :: thesis: contradiction

hence contradiction by U, A1, A2, A3, A6; :: thesis: verum

end;

suppose y1 > y2 ; :: thesis: contradiction

hence contradiction by U, A1, A2, A3, A6; :: thesis: verum

end;

end;

end;

then card M = card (Seg (n + 1)) by A, C, CARD_1:70
.= n + 1 by FINSEQ_1:57 ;
hence card M = n + 1 ; :: thesis: verum

end;

then card M > n by NAT_1:13;
then M is linearly-dependent by H, AS, lemlin;
then consider l being Linear_Combination of M such that
D1: ( Sum l = 0. (VecSp (E,F)) & Carrier l <> {} ) by VECTSP_7:def 1;
set z = the Element of Carrier l;
consider v being Element of (VecSp (E,F)) such that
D2: ( the Element of Carrier l = v & l . v <> 0. F ) by D1, VECTSP_6:1;
Carrier l c= M by VECTSP_6:def 4;
then the Element of Carrier l in M by D1;
then consider i being Element of NAT such that
D3: ( the Element of Carrier l = a |^ i & i <= n ) ;
consider pM being Polynomial of F such that
D4a: ( deg pM <= n & ( for i being Element of NAT st i <= n holds
pM . i = l . (a |^ i) ) ) by FIELD_6:47;
pM . i <> 0. F by D3, D2, D4a;
then pM <> 0_. F ;
then reconsider pM = pM as non zero Polynomial of F by UPROOTS:def 5;
Ext_eval (pM,a) = 0. (VecSp (E,F)) by U, D1, D4a, FIELD_6:49
.= 0. E by FIELD_4:def 6 ;
hence a is F -algebraic by FIELD_6:43; :: thesis: verum

end;

end;

end;

hence E is F -algebraic ; :: thesis: verum