for F being Field
for E being b₁ -finite FieldExtension of F
for K being b₁ -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 = {}