:: deftheorem lif defines lift FIELD_7:def 10 :
for F being Field
for E being b₁ -finite FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E))
for l1 being Linear_Combination of BK
for b₇ being Linear_Combination of Base (BE,BK) holds
( b₇ = lift (l1,BE) iff for b being Element of K st b in BK holds
ex l2 being Linear_Combination of BE st
( Sum l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
b₇ . (a * b) = l2 . a ) ) );