reconsider E = F as FieldExtension of F by Th3;
take
E
; 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 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 ;
( 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))
;
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 S1[
object ,
object ]
means ( (
F = e &
c2 = a ) or (
F <> e &
c2 = 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 &
S1[
x,
y] )
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
S1[
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 =
f as
Linear_Combination of
VecSp (
E,
F)
by VECTSP_6:def 1;
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 }
;
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; verum