reconsider E = F as FieldExtension of F by Th3;
take E ; :: thesis: E is F -finite
set V = VecSp (E,F);
A1: the carrier of (VecSp (E,F)) = the carrier of E by Def5;
reconsider e = 1. E as Vector of (VecSp (E,F)) by Def5;
for x being object st x in {(1. E)} holds
x in the carrier of (VecSp (E,F)) by A1;
then reconsider A = {e} as Subset of (VecSp (E,F)) by TARSKI:def 3;
0. (VecSp (E,F)) = 0. E by Def5;
then A2: A is linearly-independent by VECTSP_7:3;
A3: the carrier of (Lin A) = { (Sum l) where l is Linear_Combination of A : verum } by VECTSP_7:def 2;

A4: now :: thesis: for o being object st o in the carrier of (VecSp (E,F)) holds
o in { (Sum l) where l is Linear_Combination of A : verum }

let o be object ; :: thesis: ( o in the carrier of (VecSp (E,F)) implies o in { (Sum l) where l is Linear_Combination of A : verum } )
assume o in the carrier of (VecSp (E,F)) ; :: thesis: o in { (Sum l) where l is Linear_Combination of A : verum }
then reconsider v = o as Element of the carrier of (VecSp (E,F)) ;
reconsider a = v as Element of E by Def5;
defpred S₁[ object , object ] means ( ( F = e & c₂ = a ) or ( F <> e & c₂ = 0. E ) );
A6: for x being object st x in the carrier of (VecSp (E,F)) holds
ex y being object st
( y in the carrier of E & S₁[x,y] )

proof

let o be object ; :: thesis: ( o in the carrier of (VecSp (E,F)) implies ex y being object st
( y in the carrier of E & S₁[o,y] ) )
assume o in the carrier of (VecSp (E,F)) ; :: thesis: ex y being object st
( y in the carrier of E & S₁[o,y] )

per cases ( o = e or o <> e ) ;

suppose A7: o = e ; :: thesis: ex y being object st
( y in the carrier of E & S₁[o,y] )

take a ; :: thesis: ( a in the carrier of E & S₁[o,a] )
thus ( a in the carrier of E & S₁[o,a] ) by A7; :: thesis: verum

end;

suppose A8: o <> e ; :: thesis: ex y being object st
( y in the carrier of E & S₁[o,y] )

take 0. E ; :: thesis: ( 0. E in the carrier of E & S₁[o, 0. E] )
thus ( 0. E in the carrier of E & S₁[o, 0. E] ) by A8; :: thesis: verum

end;

end;

end;

consider f being Function of the carrier of (VecSp (E,F)), the carrier of E such that
A9: for x being object st x in the carrier of (VecSp (E,F)) holds
S₁[x,f . x] from FUNCT_2:sch 1(A6);
( dom f = the carrier of (VecSp (E,F)) & rng f c= the carrier of E ) by RELAT_1:def 19, FUNCT_2:def 1;
then reconsider f = f as Element of Funcs ( the carrier of (VecSp (E,F)), the carrier of E) by FUNCT_2:def 2;
ex T being finite Subset of (VecSp (E,F)) st
for v being Element of (VecSp (E,F)) st not v in T holds
f . v = 0. E

proof

e in the carrier of (VecSp (E,F)) ;
then for x being object st x in {e} holds
x in the carrier of (VecSp (E,F)) by TARSKI:def 1;
then reconsider T = {e} as finite Subset of (VecSp (E,F)) by TARSKI:def 3;
take T ; :: thesis: for v being Element of (VecSp (E,F)) st not v in T holds
f . v = 0. E

now :: thesis: for u being Element of (VecSp (E,F)) st not u in T holds
f . u = 0. E

let u be Element of (VecSp (E,F)); :: thesis: ( not u in T implies f . u = 0. E )
assume not u in T ; :: thesis: f . u = 0. E
then u <> e by TARSKI:def 1;
hence f . u = 0. E by A9; :: thesis: verum

end;

hence for v being Element of (VecSp (E,F)) st not v in T holds
f . v = 0. E ; :: thesis: verum

end;

then reconsider l = f as Linear_Combination of VecSp (E,F) by VECTSP_6:def 1;

now :: thesis: for o being object st o in Carrier l holds
o in A

let o be object ; :: thesis: ( o in Carrier l implies o in A )
assume o in Carrier l ; :: thesis: o in A
then o in { v where v is Element of (VecSp (E,F)) : l . v <> 0. E } by VECTSP_6:def 2;
then consider u being Element of (VecSp (E,F)) such that
A10: ( o = u & l . u <> 0. E ) ;
u = e by A10, A9;
hence o in A by A10, TARSKI:def 1; :: thesis: verum

end;

then Carrier l c= A ;
then reconsider l = l as Linear_Combination of A by VECTSP_6:def 4;
Sum l = (l . e) * e by VECTSP_6:17
.= ( the multF of E | [: the carrier of F, the carrier of E:]) . ((l . e),e) by Def5
.= a * (1. E) by A9
.= v ;
hence o in { (Sum l) where l is Linear_Combination of A : verum } ; :: thesis: verum

end;

now :: thesis: for o being object st o in { (Sum l) where l is Linear_Combination of A : verum } holds
o in the carrier of (VecSp (E,F))

let o be object ; :: thesis: ( o in { (Sum l) where l is Linear_Combination of A : verum } implies o in the carrier of (VecSp (E,F)) )
assume o in { (Sum l) where l is Linear_Combination of A : verum } ; :: thesis: o in the carrier of (VecSp (E,F))
then consider l being Linear_Combination of A such that
A11: o = Sum l ;
thus o in the carrier of (VecSp (E,F)) by A11; :: thesis: verum

end;

then the carrier of (VecSp (E,F)) = { (Sum l) where l is Linear_Combination of A : verum } by A4, TARSKI:2;
then A is Basis of (VecSp (E,F)) by A3, A2, VECTSP_4:31, VECTSP_7:def 3;
hence E is F -finite by MATRLIN:def 1; :: thesis: verum