let F be Field; :: thesis: for E being FieldExtension of F holds
( deg (E,F) = 1 iff {(1. E)} is Basis of (VecSp (E,F)) )
let E be FieldExtension of F; :: thesis: ( deg (E,F) = 1 iff {(1. E)} is Basis of (VecSp (E,F)) )
set V = VecSp (E,F);
H0: ( F is Subring of E & F is Subfield of E ) by FIELD_4:def 1, FIELD_4:7;
reconsider e = 1. E as Element of (VecSp (E,F)) by FIELD_4:def 6;

Z: now :: thesis: ( deg (E,F) = 1 implies {(1. E)} is Basis of (VecSp (E,F)) )

assume deg (E,F) = 1 ; :: thesis: {(1. E)} is Basis of (VecSp (E,F))
then AS1: the carrier of E = the carrier of F by quah1;
reconsider A = {e} as Subset of (VecSp (E,F)) ;
0. (VecSp (E,F)) = 0. E by FIELD_4:def 6;
then L: A is linearly-independent by VECTSP_7:3;
H1: the carrier of (Lin A) = { (Sum l) where l is Linear_Combination of A : verum } by VECTSP_7:def 2;

H2: 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 FIELD_4:def 6;
defpred S₁[ object , object ] means ( ( $1 = e & $2 = a ) or ( $1 <> e & $2 = 0. E ) );
G0: 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 A: 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 A; :: thesis: verum

end;

suppose A: 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 A; :: thesis: verum

end;

end;

end;

consider f being Function of the carrier of (VecSp (E,F)), the carrier of E such that
G1: for x being object st x in the carrier of (VecSp (E,F)) holds
S₁[x,f . x] from FUNCT_2:sch 1(G0);
( dom f = the carrier of (VecSp (E,F)) & rng f c= the carrier of E ) by FUNCT_2:def 1;
then reconsider f = f as Element of Funcs ( the carrier of (VecSp (E,F)), the carrier of F) by AS1, 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. F

proof

reconsider T = {e} as finite Subset of (VecSp (E,F)) ;
take T ; :: thesis: for v being Element of (VecSp (E,F)) st not v in T holds
f . v = 0. F

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

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

end;

hence for v being Element of (VecSp (E,F)) st not v in T holds
f . v = 0. F ; :: 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. F } by VECTSP_6:def 2;
then consider u being Element of (VecSp (E,F)) such that
I: ( o = u & l . u <> 0. F ) ;
l . u <> 0. E by I, H0, C0SP1:def 3;
then u = e by G1;
hence o in A by I, 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 FIELD_4:def 6
.= a * (1. E) by AS1, G1
.= 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
G: o = Sum l ;
thus o in the carrier of (VecSp (E,F)) by G; :: thesis: verum

end;

then the carrier of (VecSp (E,F)) = { (Sum l) where l is Linear_Combination of A : verum } by H2, TARSKI:2;
hence {(1. E)} is Basis of (VecSp (E,F)) by H1, L, VECTSP_4:31, VECTSP_7:def 3; :: thesis: verum

end;

now :: thesis: ( {(1. E)} is Basis of (VecSp (E,F)) implies deg (E,F) = 1 )

assume M: {(1. E)} is Basis of (VecSp (E,F)) ; :: thesis: deg (E,F) = 1
H4: card {(1. E)} = 1 by CARD_1:30;
H5: VecSp (E,F) is finite-dimensional by M, MATRLIN:def 1;
then dim (VecSp (E,F)) = 1 by M, H4, VECTSP_9:def 1;
hence deg (E,F) = 1 by H5, FIELD_4:def 7; :: thesis: verum

end;

hence ( deg (E,F) = 1 iff {(1. E)} is Basis of (VecSp (E,F)) ) by Z; :: thesis: verum