theorem LSum1: :: FIELD_7:25

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
down l = (down l1) + (down l2)