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
down l = (down l1) + (down l2)
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
down l = (down l1) + (down l2)
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
down l = (down l1) + (down l2)
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
down l = (down l1) + (down l2)
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
down l = (down l1) + (down l2)
let l, l1, l2 be Linear_Combination of Base (BE,BK); :: thesis: ( l = l1 + l2 implies down l = (down l1) + (down l2) )
assume AS: l = l1 + l2 ; :: thesis: down l = (down l1) + (down l2)

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

let o be object ; :: thesis: ( o in the carrier of (VecSp (K,E)) implies (down l) . b₁ = ((down l1) + (down l2)) . b₁ )
assume A0: o in the carrier of (VecSp (K,E)) ; :: thesis: (down l) . b₁ = ((down l1) + (down l2)) . b₁
then reconsider b = o as Element of K by FIELD_4:def 6;
reconsider bV = o as Element of (VecSp (K,E)) by A0;
H1: ( Carrier (down l) c= BK & Carrier (down l1) c= BK & Carrier (down l2) c= BK ) by VECTSP_6:def 4;

per cases ( b in BK or not b in BK ) ;

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

then A2: (down l1) . b = Sum (down (l1,b)) by down2;
(down l) . b = Sum (down (l,b)) by A1, down2
.= Sum ((down (l1,b)) + (down (l2,b))) by AS, LSum1a
.= (Sum (down (l1,b))) + (Sum (down (l2,b))) by VECTSP_6:44
.= the addF of E . [(Sum (down (l1,b))),(Sum (down (l2,b)))] by FIELD_4:def 6
.= ((down l1) . bV) + ((down l2) . bV) by A1, A2, down2 ;
hence (down l) . o = ((down l1) + (down l2)) . o by VECTSP_6:22; :: thesis: verum

end;

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

then (down l) . bV = 0. E by H1, VECTSP_6:2
.= ((down l1) . bV) + (0. E) by A1, H1, VECTSP_6:2
.= ((down l1) . bV) + ((down l2) . bV) by A1, H1, VECTSP_6:2 ;
hence (down l) . o = ((down l1) + (down l2)) . o by VECTSP_6:22; :: thesis: verum

end;

end;

end;

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