theorem :: FLEXARY1:19

for k, n being Nat
for g, h being complex-valued FinSequence holds ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g))))