:: deftheorem down2 defines down FIELD_7:def 9 :
for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being non empty finite linearly-independent Subset of (VecSp (E,F))
for BK being non empty finite linearly-independent Subset of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK)
for b₇ being Linear_Combination of BK holds
( b₇ = down l iff for b being Element of K st b in BK holds
b₇ . b = Sum (down (l,b)) );