theorem LSum1a: :: FIELD_7:24

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, l1, l2 being Linear_Combination of Base (BE,BK) st l = l1 + l2 holds
for b being Element of K holds down (l,b) = (down (l1,b)) + (down (l2,b))