let k, n be Nat; :: thesis: for g, h being complex-valued FinSequence st k <= n & n <= len g holds
((g ^ h),k) +...+ ((g ^ h),n) = (g,k) +...+ (g,n)
let g, h be complex-valued FinSequence; :: thesis: ( k <= n & n <= len g implies ((g ^ h),k) +...+ ((g ^ h),n) = (g,k) +...+ (g,n) )
set gh = g ^ h;
assume A1: ( k <= n & n <= len g ) ; :: thesis: ((g ^ h),k) +...+ ((g ^ h),n) = (g,k) +...+ (g,n)
then consider w being complex-valued FinSequence such that
A2: ( ((g ^ h),k) +...+ ((g ^ h),n) = Sum w & len w = (n -' k) + 1 ) and
A3: w . (0 + 1) = (g ^ h) . (0 + k) & ... & w . ((n -' k) + 1) = (g ^ h) . ((n -' k) + k) by Th9;
A4: ( (n -' k) + k = n & n -' k = n - k ) by A1, XREAL_1:235, XREAL_1:233;
A5: w | ((n -' k) + 1) = w by A2, FINSEQ_1:58;
w . (0 + 1) = g . (0 + k) & ... & w . ((n -' k) + 1) = g . ((n -' k) + k)

proof

let i be Nat; :: thesis: ( not 0 <= i or not i <= n -' k or w . (i + 1) = g . (i + k) )
assume A6: ( 0 <= i & i <= n -' k ) ; :: thesis: w . (i + 1) = g . (i + k)
then A7: i + k <= n by A4, XREAL_1:6;

per cases ( i + k = 0 or i + k > 0 ) ;

suppose A8: i + k = 0 ; :: thesis: w . (i + 1) = g . (i + k)

then ( not i + k in dom g & not i + k in dom (g ^ h) ) by FINSEQ_3:25;
then ( (g ^ h) . 0 = 0 & g . 0 = 0 ) by A8, FUNCT_1:def 2;
hence w . (i + 1) = g . (i + k) by A3, A8, A6; :: thesis: verum

end;

suppose i + k > 0 ; :: thesis: w . (i + 1) = g . (i + k)

then A9: i + k >= 1 by NAT_1:14;
i + k <= len g by A1, A7, XXREAL_0:2;
then i + k in dom g by A9, FINSEQ_3:25;
then g . (i + k) = (g ^ h) . (i + k) by FINSEQ_1:def 7;
hence w . (i + 1) = g . (i + k) by A3, A6; :: thesis: verum

end;

end;

end;

hence ((g ^ h),k) +...+ ((g ^ h),n) = (g,k) +...+ (g,n) by A1, Def1, A5, A2; :: thesis: verum