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 BK holds down (lift (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 BK holds down (lift (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 BK holds down (lift (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 BK holds down (lift (l,BE)) = l
let BK be Basis of (VecSp (K,E)); :: thesis: for l being Linear_Combination of BK holds down (lift (l,BE)) = l
let l1 be Linear_Combination of BK; :: thesis: down (lift (l1,BE)) = l1
H1: ( the carrier of (VecSp (K,E)) = the carrier of K & the carrier of (VecSp (E,F)) = the carrier of E ) by FIELD_4:def 6;
E is Subring of K by FIELD_4:def 1;
then H3: the carrier of E c= the carrier of K by C0SP1:def 3;
H4: Carrier l1 c= BK by VECTSP_6:def 4;

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

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

per cases ( b in BK or not b in BK ) ;

suppose X: b in BK ; :: thesis: (down (lift (l1,BE))) . b₁ = l1 . b₁

then consider l2 being Linear_Combination of BE such that
A: ( Sum l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
(lift (l1,BE)) . (a * b) = l2 . a ) ) by lif;
C: Carrier l2 c= BE by VECTSP_6:def 4;
down ((lift (l1,BE)),b) = l2

proof

now :: thesis: for o being object st o in the carrier of (VecSp (E,F)) holds
(down ((lift (l1,BE)),b)) . o = l2 . o

let o be object ; :: thesis: ( o in the carrier of (VecSp (E,F)) implies (down ((lift (l1,BE)),b)) . b₁ = l2 . b₁ )
assume AS: o in the carrier of (VecSp (E,F)) ; :: thesis: (down ((lift (l1,BE)),b)) . b₁ = l2 . b₁
then reconsider a = o as Element of K by H1, H3;
reconsider aV = o as Element of (VecSp (E,F)) by AS;

per cases ( a in BE or not a in BE ) ;

suppose Y: a in BE ; :: thesis: (down ((lift (l1,BE)),b)) . b₁ = l2 . b₁

then Z: a * b in Base (BE,BK) by X;
(down ((lift (l1,BE)),b)) . a = (lift (l1,BE)) . (a * b) by X, Y, down1
.= l2 . a by A, Y, Z ;
hence (down ((lift (l1,BE)),b)) . o = l2 . o ; :: thesis: verum

end;

suppose AS1: not a in BE ; :: thesis: (down ((lift (l1,BE)),b)) . b₁ = l2 . b₁

then D: l2 . aV = 0. F by C, VECTSP_6:2;
Carrier (down ((lift (l1,BE)),b)) c= BE by VECTSP_6:def 4;
hence (down ((lift (l1,BE)),b)) . o = l2 . o by D, AS1, VECTSP_6:2; :: thesis: verum

end;

end;

end;

hence down ((lift (l1,BE)),b) = l2 ; :: thesis: verum

end;

hence (down (lift (l1,BE))) . o = l1 . o by A, X, down2; :: thesis: verum

end;

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

then A: l1 . bV = 0. E by H4, VECTSP_6:2;
Carrier (down (lift (l1,BE))) c= BK by VECTSP_6:def 4;
hence (down (lift (l1,BE))) . o = l1 . o by A, X, VECTSP_6:2; :: thesis: verum

end;

end;

end;

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