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)) holds Base (BE,BK) is Basis of (VecSp (K,F))
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)) holds Base (BE,BK) is Basis of (VecSp (K,F))
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)) holds Base (BE,BK) is Basis of (VecSp (K,F))
let BE be Basis of (VecSp (E,F)); :: thesis: for BK being Basis of (VecSp (K,E)) holds Base (BE,BK) is Basis of (VecSp (K,F))
let BK be Basis of (VecSp (K,E)); :: thesis: Base (BE,BK) is Basis of (VecSp (K,F))
A: for l being Linear_Combination of Base (BE,BK) st Sum l = 0. (VecSp (K,F)) holds
Carrier l = {} by T1;
Lin (Base (BE,BK)) = ModuleStr(# the carrier of (VecSp (K,F)), the addF of (VecSp (K,F)), the ZeroF of (VecSp (K,F)), the lmult of (VecSp (K,F)) #) by T2;
hence Base (BE,BK) is Basis of (VecSp (K,F)) by A, VECTSP_7:def 1, VECTSP_7:def 3; :: thesis: verum