:: deftheorem down1 defines down FIELD_7:def 8 :
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 linearly-independent Subset of (VecSp (K,E))
for l being Linear_Combination of Base (BE,BK)
for b being Element of K
for b₈ being Linear_Combination of BE holds
( b₈ = down (l,b) iff ( ( for a being Element of K st a in BE & b in BK holds
b₈ . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
b₈ . a = 0. F ) ) );