for k being Nat
for h being complex-valued FinSequence holds (h,0) +...+ (h,k) = (h,1) +...+ (h,k)