let F be Field; :: thesis: for E being FieldExtension of F
for K being F -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))
let E be FieldExtension of F; :: thesis: for K being F -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))
let K be F -extending FieldExtension of F; :: thesis: 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))
let BE be non empty finite linearly-independent Subset of (VecSp (E,F)); :: thesis: 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))
let BK be non empty finite linearly-independent Subset of (VecSp (K,E)); :: thesis: 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))
let l, l1, l2 be Linear_Combination of Base (BE,BK); :: thesis: ( l = l1 + l2 implies for b being Element of K holds down (l,b) = (down (l1,b)) + (down (l2,b)) )
assume AS: l = l1 + l2 ; :: thesis: for b being Element of K holds down (l,b) = (down (l1,b)) + (down (l2,b))
let b be Element of K; :: thesis: down (l,b) = (down (l1,b)) + (down (l2,b))
E is Subring of K by FIELD_4:def 1;
then X1: the carrier of E c= the carrier of K by C0SP1:def 3;

now :: thesis: for o being object st o in the carrier of (VecSp (E,F)) holds
(down (l,b)) . o = ((down (l1,b)) + (down (l2,b))) . o

let o be object ; :: thesis: ( o in the carrier of (VecSp (E,F)) implies (down (l,b)) . b₁ = ((down (l1,b)) + (down (l2,b))) . b₁ )
assume A0: o in the carrier of (VecSp (E,F)) ; :: thesis: (down (l,b)) . b₁ = ((down (l1,b)) + (down (l2,b))) . b₁
then A2: o in the carrier of E by FIELD_4:def 6;
then reconsider a = o as Element of K by X1;
reconsider aE = o as Element of E by A0, FIELD_4:def 6;
reconsider aV = o as Element of (VecSp (E,F)) by A0;
reconsider abV = a * b as Element of (VecSp (K,F)) by FIELD_4:def 6;

per cases ( ( a in BE & b in BK ) or not a in BE or not b in BK ) ;

suppose A1: ( a in BE & b in BK ) ; :: thesis: (down (l,b)) . b₁ = ((down (l1,b)) + (down (l2,b))) . b₁

then (down (l,b)) . a = l . (a * b) by down1
.= (l1 . abV) + (l2 . abV) by AS, VECTSP_6:22
.= the addF of F . [((down (l1,b)) . a),(l2 . abV)] by A1, down1
.= ((down (l1,b)) . aV) + ((down (l2,b)) . aV) by A1, down1
.= ((down (l1,b)) + (down (l2,b))) . aV by VECTSP_6:22 ;
hence (down (l,b)) . o = ((down (l1,b)) + (down (l2,b))) . o ; :: thesis: verum

end;

suppose A1: ( not a in BE or not b in BK ) ; :: thesis: (down (l,b)) . b₁ = ((down (l1,b)) + (down (l2,b))) . b₁

then A3: ( (down (l1,b)) . a = 0. F & (down (l2,b)) . a = 0. F ) by A2, down1;
(down (l,b)) . a = ((down (l1,b)) . aV) + ((down (l2,b)) . aV) by A3, A1, A2, down1;
hence (down (l,b)) . o = ((down (l1,b)) + (down (l2,b))) . o by VECTSP_6:22; :: thesis: verum

end;

end;

end;

hence down (l,b) = (down (l1,b)) + (down (l2,b)) ; :: thesis: verum