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 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)) #)
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 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)) #)
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 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)) #)
let BE be Basis of (VecSp (E,F)); :: thesis: for BK being Basis of (VecSp (K,E)) holds 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)) #)
let BK be Basis of (VecSp (K,E)); :: thesis: 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)) #)
set V = VecSp (K,F);
H1: the carrier of (VecSp (K,F)) = the carrier of K by FIELD_4:def 6;
H2: ( Lin BE = ModuleStr(# the carrier of (VecSp (E,F)), the addF of (VecSp (E,F)), the ZeroF of (VecSp (E,F)), the lmult of (VecSp (E,F)) #) & Lin BK = ModuleStr(# the carrier of (VecSp (K,E)), the addF of (VecSp (K,E)), the ZeroF of (VecSp (K,E)), the lmult of (VecSp (K,E)) #) ) by VECTSP_7:def 3;

A: now :: thesis: for o being object st o in the carrier of (VecSp (K,F)) holds
o in the carrier of (Lin (Base (BE,BK)))

let o be object ; :: thesis: ( o in the carrier of (VecSp (K,F)) implies o in the carrier of (Lin (Base (BE,BK))) )
assume o in the carrier of (VecSp (K,F)) ; :: thesis: o in the carrier of (Lin (Base (BE,BK)))
then o in Lin BK by H1, H2, FIELD_4:def 6;
then consider l1 being Linear_Combination of BK such that
A0: o = Sum l1 by VECTSP_7:7;
set l = lift (l1,BE);
down (lift (l1,BE)) = l1 by Tlift2;
then Sum (lift (l1,BE)) = o by A0, TSum;
then o in { (Sum l) where l is Linear_Combination of Base (BE,BK) : verum } ;
hence o in the carrier of (Lin (Base (BE,BK))) by VECTSP_7:def 2; :: thesis: verum

end;

now :: thesis: for o being object st o in the carrier of (Lin (Base (BE,BK))) holds
o in the carrier of (VecSp (K,F))

let o be object ; :: thesis: ( o in the carrier of (Lin (Base (BE,BK))) implies o in the carrier of (VecSp (K,F)) )
assume A: o in the carrier of (Lin (Base (BE,BK))) ; :: thesis: o in the carrier of (VecSp (K,F))
the carrier of (Lin (Base (BE,BK))) = { (Sum l) where l is Linear_Combination of Base (BE,BK) : verum } by VECTSP_7:def 2;
then consider l1 being Linear_Combination of Base (BE,BK) such that
B: o = Sum l1 by A;
thus o in the carrier of (VecSp (K,F)) by B; :: thesis: verum

end;

hence 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 A, TARSKI:2, VECTSP_4:31; :: thesis: verum