let k be Nat; :: thesis: for h being complex-valued FinSequence holds (h,0) +...+ (h,k) = (h,1) +...+ (h,k)
let h be complex-valued FinSequence; :: thesis: (h,0) +...+ (h,k) = (h,1) +...+ (h,k)
not 0 in dom h by FINSEQ_3:25;
then A1: h . 0 = 0 by FUNCT_1:def 2;
(h,0) +...+ (h,k) = (h . 0) + ((h,(0 + 1)) +...+ (h,k)) by Th13;
hence (h,0) +...+ (h,k) = (h,1) +...+ (h,k) by A1; :: thesis: verum