let k, n be Nat; 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; ( 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 )
; ((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)
hence
((g ^ h),k) +...+ ((g ^ h),n) = (g,k) +...+ (g,n)
by A1, Def1, A5, A2; verum