let k, n be Nat; for g, h being complex-valued FinSequence st k <= n & k > len g holds
((g ^ h),k) +...+ ((g ^ h),n) = (h,(k -' (len g))) +...+ (h,(n -' (len g)))
let g, h be complex-valued FinSequence; ( k <= n & k > len g implies ((g ^ h),k) +...+ ((g ^ h),n) = (h,(k -' (len g))) +...+ (h,(n -' (len g))) )
set gh = g ^ h;
assume A1:
( k <= n & k > len g )
; ((g ^ h),k) +...+ ((g ^ h),n) = (h,(k -' (len g))) +...+ (h,(n -' (len g)))
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;
set kL = k -' (len g);
set nL = n -' (len g);
A6:
( k -' (len g) = k - (len g) & n -' (len g) = n - (len g) )
by A1, XXREAL_0:2, XREAL_1:233;
A7:
k -' (len g) <= n -' (len g)
by A1, NAT_D:42;
A8:
(n -' (len g)) -' (k -' (len g)) = (n -' (len g)) - (k -' (len g))
by A1, NAT_D:42, XREAL_1:233;
w . (0 + 1) = h . (0 + (k -' (len g))) & ... & w . (((n -' (len g)) -' (k -' (len g))) + 1) = h . (((n -' (len g)) -' (k -' (len g))) + (k -' (len g)))
hence
((g ^ h),k) +...+ ((g ^ h),n) = (h,(k -' (len g))) +...+ (h,(n -' (len g)))
by A8, A6, A4, A5, Def1, A7, A2; verum