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;

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

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 }

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_{1}[ object , object ] means ( ( F = e & c_{2} = a ) or ( F <> e & c_{2} = 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_{1}[x,y] )

A9: for x being object st x in the carrier of (VecSp (E,F)) holds

S_{1}[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

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;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

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

proof

consider f being Function of the carrier of (VecSp (E,F)), the carrier of E such that
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_{1}[o,y] ) )

assume o in the carrier of (VecSp (E,F)) ; :: thesis: ex y being object st

( y in the carrier of E & S_{1}[o,y] )

end;( y in the carrier of E & S

assume o in the carrier of (VecSp (E,F)) ; :: thesis: ex y being object st

( y in the carrier of E & S

A9: for x being object st x in the carrier of (VecSp (E,F)) holds

S

( 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

then reconsider l = f as Linear_Combination of VecSp (E,F) by VECTSP_6:def 1;
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

f . v = 0. E ; :: thesis: verum

end;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

hence
for v being Element of (VecSp (E,F)) st not v 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;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

f . v = 0. E ; :: thesis: verum

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

o in A

then
Carrier l c= A
;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;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

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

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))

then
the carrier of (VecSp (E,F)) = { (Sum l) where l is Linear_Combination of A : verum }
by A4, TARSKI:2;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;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

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