Let K be a field and let V be a vector space over K with zero vector 0V. Let N be the set of natural numbers with successor map S as in that definition, ordered by the relation ≤ of that definition, let n∈N, and let [n] be the initial segment determined by n, that is, the set of natural numbers k with 1≤k≤n. Let u:[n]→V and v:[n]→V be maps with values uk and vk, let c:[n]→K be a map with values ck, and let λ∈K.
Sums of vectors are the finite sums in a vector space, and sums of scalars are the finite sums in a field. Then the following hold.
1. (Restriction and recursion) If j∈[n] and v′ denotes the restriction of v to [j], then
k=1∑ivk′=k=1∑ivkfor every i∈[j].
Moreover
k=1∑1vk=v1,k=1∑S(m)vk=(k=1∑mvk)+vS(m)whenever S(m)∈[n].
2. (Additivity)
k=1∑n(uk+vk)=k=1∑nuk+k=1∑nvk.
3. (Homogeneity)
k=1∑n(λvk)=λk=1∑nvk.
4. (Linear maps) Let W be a vector space over K and let T:V→W be a linear map. Then
T(k=1∑nvk)=k=1∑nT(vk),
the sum on the right being the finite sum in W.
5. (Inner products against a finite sum) Suppose K is the field of complex numbers and V together with ⟨⋅,⋅⟩ is a complex inner product space, and let w∈V. Then
⟨w,k=1∑nvk⟩=k=1∑n⟨w,vk⟩,⟨k=1∑nvk,w⟩=k=1∑n⟨vk,w⟩,
the sums on the right being finite sums in the field of complex numbers.
6. (Inner products against a linear combination) Under the hypotheses of claim 5, with the complex conjugate,
⟨w,k=1∑nckvk⟩=k=1∑nck⟨w,vk⟩,⟨k=1∑nckvk,w⟩=k=1∑nck⟨vk,w⟩.
7. (A single possibly nonzero summand) Let i∈[n] and suppose that vk=0V for every k∈[n] with k=i. Then
k=1∑nvk=vi.
In particular, if vk=0V for every k∈[n], then ∑k=1nvk=0V.