let k, n be Nat; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ((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)))

proof

let i be Nat; :: thesis: ( not 0 <= i or not i <= (n -' (len g)) -' (k -' (len g)) or w . (i + 1) = h . (i + (k -' (len g))) )
assume A9: ( 0 <= i & i <= (n -' (len g)) -' (k -' (len g)) ) ; :: thesis: w . (i + 1) = h . (i + (k -' (len g)))
then A10: w . (i + 1) = (g ^ h) . (i + k) by A8, A6, A4, A3;
k -' (len g) <> 0 by A1, A6;
then A11: (k -' (len g)) + i >= 1 + 0 by NAT_1:14;

per cases ( (k -' (len g)) + i <= len h or (k -' (len g)) + i > len h ) ;

suppose (k -' (len g)) + i <= len h ; :: thesis: w . (i + 1) = h . (i + (k -' (len g)))

then (k -' (len g)) + i in dom h by A11, FINSEQ_3:25;
then h . ((k -' (len g)) + i) = (g ^ h) . (((k -' (len g)) + i) + (len g)) by FINSEQ_1:def 7;
then h . ((k -' (len g)) + i) = (g ^ h) . (i + k) by A6;
hence w . (i + 1) = h . (i + (k -' (len g))) by A9, A8, A6, A4, A3; :: thesis: verum

end;

suppose A12: (k -' (len g)) + i > len h ; :: thesis: w . (i + 1) = h . (i + (k -' (len g)))

then not (k -' (len g)) + i in dom h by FINSEQ_3:25;
then A13: h . (i + (k -' (len g))) = 0 by FUNCT_1:def 2;
((k -' (len g)) + i) + (len g) > (len h) + (len g) by A12, XREAL_1:6;
then ( i + k > (len g) + (len h) & len (g ^ h) = (len g) + (len h) ) by A6, FINSEQ_1:22;
then not i + k in dom (g ^ h) by FINSEQ_3:25;
hence w . (i + 1) = h . (i + (k -' (len g))) by FUNCT_1:def 2, A13, A10; :: thesis: verum

end;

end;

end;

hence ((g ^ h),k) +...+ ((g ^ h),n) = (h,(k -' (len g))) +...+ (h,(n -' (len g))) by A8, A6, A4, A5, Def1, A7, A2; :: thesis: verum