theorem Tlift2: :: FIELD_7:23

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 BK holds down (lift (l,BE)) = l