let F be Field; :: thesis: for E being F -finite FieldExtension of F
for K being F -extending b₁ -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) st Sum l = 0. (VecSp (K,F)) holds
Carrier l = {}
let E be F -finite FieldExtension of F; :: thesis: for K being F -extending E -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) st Sum l = 0. (VecSp (K,F)) holds
Carrier l = {}
let K be F -extending E -finite FieldExtension of F; :: thesis: for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) st Sum l = 0. (VecSp (K,F)) holds
Carrier l = {}
let BE be Basis of (VecSp (E,F)); :: thesis: for BK being Basis of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK) st Sum l = 0. (VecSp (K,F)) holds
Carrier l = {}
let BK be Basis of (VecSp (K,E)); :: thesis: for l being Linear_Combination of Base (BE,BK) st Sum l = 0. (VecSp (K,F)) holds
Carrier l = {}
let l1 be Linear_Combination of Base (BE,BK); :: thesis: ( Sum l1 = 0. (VecSp (K,F)) implies Carrier l1 = {} )
set l2 = down l1;
assume AS: Sum l1 = 0. (VecSp (K,F)) ; :: thesis: Carrier l1 = {}
B: Sum (down l1) = Sum l1 by TSum
.= 0. K by AS, FIELD_4:def 6
.= 0. (VecSp (K,E)) by FIELD_4:def 6 ;
C: Carrier (down l1) = {} by B, VECTSP_7:def 1;

D: now :: thesis: for x being Element of K st x in Base (BE,BK) holds
not x in Carrier l1

let x be Element of K; :: thesis: ( x in Base (BE,BK) implies not x in Carrier l1 )
assume x in Base (BE,BK) ; :: thesis: not x in Carrier l1
then consider a, b being Element of K such that
B1: ( x = a * b & a in BE & b in BK ) ;
reconsider bv = b as Element of (VecSp (K,E)) by FIELD_4:def 6;
0. (VecSp (E,F)) = 0. E by FIELD_4:def 6
.= (down l1) . bv by C, VECTSP_6:2
.= Sum (down (l1,b)) by B1, down2 ;
then B3: Carrier (down (l1,b)) = {} by VECTSP_7:def 1;
reconsider av = a as Element of (VecSp (E,F)) by B1;
0. F = (down (l1,b)) . av by B3, VECTSP_6:2
.= l1 . (a * b) by B1, down1 ;
hence not x in Carrier l1 by B1, VECTSP_6:2; :: thesis: verum

end;

now :: thesis: for o being object holds not o in Carrier l1

let o be object ; :: thesis: not o in Carrier l1
assume C1: o in Carrier l1 ; :: thesis: contradiction
then reconsider x = o as Element of K by FIELD_4:def 6;
Carrier l1 c= Base (BE,BK) by VECTSP_6:def 4;
then x in Base (BE,BK) by C1;
hence contradiction by D, C1; :: thesis: verum

end;

hence Carrier l1 = {} by XBOOLE_0:def 1; :: thesis: verum