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) holds lift ((down l),BE) = 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) holds lift ((down l),BE) = 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) holds lift ((down l),BE) = 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) holds lift ((down l),BE) = l
let BK be Basis of (VecSp (K,E)); :: thesis: for l being Linear_Combination of Base (BE,BK) holds lift ((down l),BE) = l
let l be Linear_Combination of Base (BE,BK); :: thesis: lift ((down l),BE) = l
H4: Carrier l c= Base (BE,BK) by VECTSP_6:def 4;

now :: thesis: for o being object st o in the carrier of (VecSp (K,F)) holds
l . o = (lift ((down l),BE)) . o

let o be object ; :: thesis: ( o in the carrier of (VecSp (K,F)) implies l . b₁ = (lift ((down l),BE)) . b₁ )
assume AS: o in the carrier of (VecSp (K,F)) ; :: thesis: l . b₁ = (lift ((down l),BE)) . b₁
then reconsider c = o as Element of K by FIELD_4:def 6;
reconsider cV = o as Element of (VecSp (K,F)) by AS;

per cases ( c in Base (BE,BK) or not c in Base (BE,BK) ) ;

suppose AS: c in Base (BE,BK) ; :: thesis: l . b₁ = (lift ((down l),BE)) . b₁

then consider a, b being Element of K such that
A: ( c = a * b & a in BE & b in BK ) ;
B: (down l) . b = Sum (down (l,b)) by A, down2;
consider l2 being Linear_Combination of BE such that
D: ( Sum l2 = (down l) . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
(lift ((down l),BE)) . (a * b) = l2 . a ) ) by A, lif;
l2 = down (l,b) by D, B, ZMODUL033;
then (lift ((down l),BE)) . (a * b) = (down (l,b)) . a by A, D, AS
.= l . (a * b) by A, down1 ;
hence l . o = (lift ((down l),BE)) . o by A; :: thesis: verum

end;

suppose X: not c in Base (BE,BK) ; :: thesis: l . b₁ = (lift ((down l),BE)) . b₁

then A: l . cV = 0. F by H4, VECTSP_6:2;
Carrier (lift ((down l),BE)) c= Base (BE,BK) by VECTSP_6:def 4;
hence l . o = (lift ((down l),BE)) . o by A, X, VECTSP_6:2; :: thesis: verum

end;

end;

end;

hence lift ((down l),BE) = l ; :: thesis: verum